case h
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Fintype ι
b : Basis ι R M
f : Dual R M
m : M
⊢ ↑(∑ x : ι, ↑f (↑b x) • coord b x) m = ↑f m
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Fintype ι
b : Basis ι R M
f : Dual R M
⊢ ∑ x : ι, ↑f (↑b x) • coord b x = f
ext m
no goals
case h
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Fintype ι
b : Basis ι R M
f : Dual R M
m : M
⊢ ↑(∑ x : ι, ↑f (↑b x) • coord b x) m = ↑f m
simp_rw [LinearMap.sum_apply, LinearMap.smul_apply, smul_eq_mul, mul_comm (f _), ← smul_eq_mul, ←
  f.map_smul, ← f.map_sum, Basis.coord_apply, Basis.sum_repr]