From 83413722b6c27529538985583d00dd817805f440 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Tue, 22 Oct 2024 17:53:01 +0000 Subject: [PATCH] fix --- Mathlib/LinearAlgebra/Multilinear/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/Multilinear/Basic.lean b/Mathlib/LinearAlgebra/Multilinear/Basic.lean index 39f1d7e414a2b0..c51826cc4424cb 100644 --- a/Mathlib/LinearAlgebra/Multilinear/Basic.lean +++ b/Mathlib/LinearAlgebra/Multilinear/Basic.lean @@ -152,7 +152,7 @@ protected theorem map_smul [DecidableEq ι] (m : ∀ i, M₁ i) (i : ι) (c : R) theorem map_coord_zero {m : ∀ i, M₁ i} (i : ι) (h : m i = 0) : f m = 0 := by classical have : (0 : R) • (0 : M₁ i) = 0 := by simp - rw [← update_eq_self i m, h, ← this, f.map_smul, zero_smul R (M := M₂)] + rw [← update_eq_self i m, h, ← this, f.map_smul, zero_smul R (A := M₂)] @[simp] theorem map_update_zero [DecidableEq ι] (m : ∀ i, M₁ i) (i : ι) : f (update m i 0) = 0 :=