case a.h
ι : Type u_1
ι' : Type ?u.55138
κ : Type ?u.55141
κ' : Type ?u.55144
R : Type u_2
M : Type u_3
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
R₂ : Type ?u.55337
M₂ : Type ?u.55340
inst✝⁴ : CommRing R₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R₂ M₂
e : Basis ι R M
v✝ : ι' → M
i : ι
j : ι'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
v : ι → M
i✝ x✝ : ι
⊢ toMatrix e v i✝ x✝ = ↑(LinearMap.toMatrix e e) (↑(constr e ℕ) v) i✝ x✝
ι : Type u_1
ι' : Type ?u.55138
κ : Type ?u.55141
κ' : Type ?u.55144
R : Type u_2
M : Type u_3
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
R₂ : Type ?u.55337
M₂ : Type ?u.55340
inst✝⁴ : CommRing R₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R₂ M₂
e : Basis ι R M
v✝ : ι' → M
i : ι
j : ι'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
v : ι → M
⊢ toMatrix e v = ↑(LinearMap.toMatrix e e) (↑(constr e ℕ) v)
ext
no goals
case a.h
ι : Type u_1
ι' : Type ?u.55138
κ : Type ?u.55141
κ' : Type ?u.55144
R : Type u_2
M : Type u_3
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
R₂ : Type ?u.55337
M₂ : Type ?u.55340
inst✝⁴ : CommRing R₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R₂ M₂
e : Basis ι R M
v✝ : ι' → M
i : ι
j : ι'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
v : ι → M
i✝ x✝ : ι
⊢ toMatrix e v i✝ x✝ = ↑(LinearMap.toMatrix e e) (↑(constr e ℕ) v) i✝ x✝
rw [Basis.toMatrix_apply, LinearMap.toMatrix_apply, Basis.constr_basis]