case h.a.h
ι : Type u_1
ι' : Type ?u.96253
κ : Type ?u.96256
κ' : Type ?u.96259
R : Type u_2
M✝ : Type ?u.96265
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M✝
inst✝⁴ : Module R M✝
R₂ : Type ?u.96452
M₂ : Type ?u.96455
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e : Basis ι R M✝
v : ι' → M✝
i✝ : ι
j✝ : ι'
inst✝ : Fintype ι
M : ι → ι → R
i j : ι
⊢ toMatrix (Pi.basisFun R ι) M i j = Mᵀ i j
ι : Type u_1
ι' : Type ?u.96253
κ : Type ?u.96256
κ' : Type ?u.96259
R : Type u_2
M : Type ?u.96265
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type ?u.96452
M₂ : Type ?u.96455
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
inst✝ : Fintype ι
⊢ toMatrix (Pi.basisFun R ι) = transpose
ext (M i j)
no goals
case h.a.h
ι : Type u_1
ι' : Type ?u.96253
κ : Type ?u.96256
κ' : Type ?u.96259
R : Type u_2
M✝ : Type ?u.96265
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M✝
inst✝⁴ : Module R M✝
R₂ : Type ?u.96452
M₂ : Type ?u.96455
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e : Basis ι R M✝
v : ι' → M✝
i✝ : ι
j✝ : ι'
inst✝ : Fintype ι
M : ι → ι → R
i j : ι
⊢ toMatrix (Pi.basisFun R ι) M i j = Mᵀ i j
rfl