case h
ι : Type u_3
ι' : Type u_4
κ : Type ?u.263788
κ' : Type ?u.263791
R : Type u_2
M : Type ?u.263797
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
R₂ : Type ?u.263984
M₂ : Type ?u.263987
inst✝⁵ : CommRing R₂
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R₂ M₂
e : Basis ι R M
v✝ : ι' → M
i✝ : ι
j : ι'
S : Type u_1
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : Fintype ι
b : Basis ι R S
v : ι' → S
i : ι'
⊢ vecMul (↑b) (Matrix.map (toMatrix b v) ↑(algebraMap R S)) i = v i
ι : Type u_3
ι' : Type u_4
κ : Type ?u.263788
κ' : Type ?u.263791
R : Type u_2
M : Type ?u.263797
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
R₂ : Type ?u.263984
M₂ : Type ?u.263987
inst✝⁵ : CommRing R₂
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R₂ M₂
e : Basis ι R M
v✝ : ι' → M
i : ι
j : ι'
S : Type u_1
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : Fintype ι
b : Basis ι R S
v : ι' → S
⊢ vecMul (↑b) (Matrix.map (toMatrix b v) ↑(algebraMap R S)) = v
ext i
no goals
case h
ι : Type u_3
ι' : Type u_4
κ : Type ?u.263788
κ' : Type ?u.263791
R : Type u_2
M : Type ?u.263797
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
R₂ : Type ?u.263984
M₂ : Type ?u.263987
inst✝⁵ : CommRing R₂
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R₂ M₂
e : Basis ι R M
v✝ : ι' → M
i✝ : ι
j : ι'
S : Type u_1
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : Fintype ι
b : Basis ι R S
v : ι' → S
i : ι'
⊢ vecMul (↑b) (Matrix.map (toMatrix b v) ↑(algebraMap R S)) i = v i
simp_rw [vecMul, dotProduct, Matrix.map_apply, ← Algebra.commutes, ← Algebra.smul_def,
  sum_toMatrix_smul_self]