case h
R : Type u_2
M : Type u_3
ι : Type u_1
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
l : ι →₀ R
i : ι
⊢ ↑(coeffs h (lc e l)) i = ↑l i
R : Type u_2
M : Type u_3
ι : Type u_1
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
l : ι →₀ R
⊢ coeffs h (lc e l) = l
ext i
no goals
case h
R : Type u_2
M : Type u_3
ι : Type u_1
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
l : ι →₀ R
i : ι
⊢ ↑(coeffs h (lc e l)) i = ↑l i
rw [h.coeffs_apply, h.dual_lc]