case a.h
R : Type u_1
inst✝⁷ : CommSemiring R
l : Type ?u.1742508
m : Type ?u.1742511
n : Type u_2
inst✝⁶ : Fintype n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq n
M₁ : Type u_3
M₂ : Type ?u.1742535
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
i j : n
⊢ ↑(toMatrix v₁ v₁) id i j = OfNat.ofNat 1 i j
R : Type u_1
inst✝⁷ : CommSemiring R
l : Type ?u.1742508
m : Type ?u.1742511
n : Type u_2
inst✝⁶ : Fintype n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq n
M₁ : Type u_3
M₂ : Type ?u.1742535
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
⊢ ↑(toMatrix v₁ v₁) id = 1
ext (i j)
no goals
case a.h
R : Type u_1
inst✝⁷ : CommSemiring R
l : Type ?u.1742508
m : Type ?u.1742511
n : Type u_2
inst✝⁶ : Fintype n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq n
M₁ : Type u_3
M₂ : Type ?u.1742535
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
i j : n
⊢ ↑(toMatrix v₁ v₁) id i j = OfNat.ofNat 1 i j
simp [LinearMap.toMatrix_apply, Matrix.one_apply, Finsupp.single_apply, eq_comm]