case a.h
R : Type u_2
inst✝¹¹ : CommSemiring R
l : Type u_1
m : Type ?u.2073940
n : Type ?u.2073943
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype m
inst✝⁸ : DecidableEq n
M₁ : Type u_3
M₂ : Type u_4
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.2074466
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₃
v₃ : Basis l R M₃
inst✝¹ : Fintype l
inst✝ : DecidableEq l
b : Basis l R M₁
b' : Basis l R M₂
i j : l
⊢ ↑(toMatrix b' b) (↑(Basis.equiv b' b (Equiv.refl l))) i j = OfNat.ofNat 1 i j
R : Type u_2
inst✝¹¹ : CommSemiring R
l : Type u_1
m : Type ?u.2073940
n : Type ?u.2073943
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype m
inst✝⁸ : DecidableEq n
M₁ : Type u_3
M₂ : Type u_4
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.2074466
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₃
v₃ : Basis l R M₃
inst✝¹ : Fintype l
inst✝ : DecidableEq l
b : Basis l R M₁
b' : Basis l R M₂
⊢ ↑(toMatrix b' b) ↑(Basis.equiv b' b (Equiv.refl l)) = 1
ext (i j)
no goals
case a.h
R : Type u_2
inst✝¹¹ : CommSemiring R
l : Type u_1
m : Type ?u.2073940
n : Type ?u.2073943
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype m
inst✝⁸ : DecidableEq n
M₁ : Type u_3
M₂ : Type u_4
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.2074466
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₃
v₃ : Basis l R M₃
inst✝¹ : Fintype l
inst✝ : DecidableEq l
b : Basis l R M₁
b' : Basis l R M₂
i j : l
⊢ ↑(toMatrix b' b) (↑(Basis.equiv b' b (Equiv.refl l))) i j = OfNat.ofNat 1 i j
simp [LinearMap.toMatrix_apply, Matrix.one_apply, Finsupp.single_apply, eq_comm]