Skip to content

Commit

Permalink
fix
Browse files Browse the repository at this point in the history
  • Loading branch information
YaelDillies committed Oct 22, 2024
1 parent a9d5fc1 commit 8341372
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/LinearAlgebra/Multilinear/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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 :=
Expand Down

0 comments on commit 8341372

Please sign in to comment.