case a.h
R : Type u_1
inst✝⁹ : CommSemiring R
l : Type ?u.2925604
m : Type ?u.2925607
n : Type u_2
inst✝⁸ : Fintype n
inst✝⁷ : Fintype m
inst✝⁶ : DecidableEq n
M₁ : Type u_3
M₂ : Type ?u.2925631
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type ?u.2926133
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
v₃ : Basis l R M₃
x : R
i✝ x✝ : n
⊢ ↑(toMatrix v₁ v₁) (DistribMulAction.toLinearMap R M₁ x) i✝ x✝ = Matrix.diagonal (fun x_1 => x) i✝ x✝
R : Type u_1
inst✝⁹ : CommSemiring R
l : Type ?u.2925604
m : Type ?u.2925607
n : Type u_2
inst✝⁸ : Fintype n
inst✝⁷ : Fintype m
inst✝⁶ : DecidableEq n
M₁ : Type u_3
M₂ : Type ?u.2925631
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type ?u.2926133
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
v₃ : Basis l R M₃
x : R
⊢ ↑(toMatrix v₁ v₁) (DistribMulAction.toLinearMap R M₁ x) = Matrix.diagonal fun x_1 => x
ext
no goals
case a.h
R : Type u_1
inst✝⁹ : CommSemiring R
l : Type ?u.2925604
m : Type ?u.2925607
n : Type u_2
inst✝⁸ : Fintype n
inst✝⁷ : Fintype m
inst✝⁶ : DecidableEq n
M₁ : Type u_3
M₂ : Type ?u.2925631
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type ?u.2926133
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
v₃ : Basis l R M₃
x : R
i✝ x✝ : n
⊢ ↑(toMatrix v₁ v₁) (DistribMulAction.toLinearMap R M₁ x) i✝ x✝ = Matrix.diagonal (fun x_1 => x) i✝ x✝
rw [LinearMap.toMatrix_apply, DistribMulAction.toLinearMap_apply, LinearEquiv.map_smul,
  Basis.repr_self, Finsupp.smul_single_one, Finsupp.single_eq_pi_single, Matrix.diagonal_apply,
  Pi.single_apply]