R : Type u_2
M : Type u_1
ι : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
m : M
⊢ ∀ (i : ι), ↑(ε i) (lc e (coeffs h m) - m) = 0
R : Type u_2
M : Type u_1
ι : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
m : M
⊢ lc e (coeffs h m) = m
refine' eq_of_sub_eq_zero (h.Total _)
R : Type u_2
M : Type u_1
ι : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
m : M
i : ι
⊢ ↑(ε i) (lc e (coeffs h m) - m) = 0
R : Type u_2
M : Type u_1
ι : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
m : M
⊢ ∀ (i : ι), ↑(ε i) (lc e (coeffs h m) - m) = 0
intro i
no goals
R : Type u_2
M : Type u_1
ι : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
m : M
i : ι
⊢ ↑(ε i) (lc e (coeffs h m) - m) = 0
simp [LinearMap.map_sub, h.dual_lc, sub_eq_zero]