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 : ι
⊢ (Finset.sum l.support fun i_1 => ↑(ε i) ((fun i a => a • e i) i_1 (↑l i_1))) = ↑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
i : ι
⊢ ↑(ε i) (lc e l) = ↑l i
erw [LinearMap.map_sum]
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 : ι
⊢ (Finset.sum l.support fun x => ↑(ε i) (↑l x • e x)) = ↑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
i : ι
⊢ (Finset.sum l.support fun i_1 => ↑(ε i) ((fun i a => a • e i) i_1 (↑l i_1))) = ↑l i
simp_rw [map_smul]
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 : ι
⊢ ↑(ε i) (↑l i • e i) = ↑l i

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 : ι
⊢ ∀ (b : ι), b ∈ l.support → b ≠ i → ↑(ε i) (↑l b • e b) = 0

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 : ι
⊢ ¬i ∈ l.support → ↑(ε i) (↑l i • e i) = 0
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 : ι
⊢ (Finset.sum l.support fun x => ↑(ε i) (↑l x • e x)) = ↑l i
rw [Finset.sum_eq_single i]
no goals
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 : ι
⊢ ↑(ε i) (↑l i • e i) = ↑l i
simp [h.eval, smul_eq_mul]
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 q : ι
a✝ : q ∈ l.support
q_ne : q ≠ i
⊢ ↑(ε i) (↑l q • e q) = 0
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 : ι
⊢ ∀ (b : ι), b ∈ l.support → b ≠ i → ↑(ε i) (↑l b • e b) = 0
intro q _ q_ne
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 q : ι
a✝ : q ∈ l.support
q_ne : q ≠ i
⊢ ↑(ε i) (↑l q • e q) = 0
simp [q_ne.symm, h.eval, smul_eq_mul]
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 : ι
p_not_in : ¬i ∈ l.support
⊢ ↑(ε i) (↑l i • e i) = 0
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 : ι
⊢ ¬i ∈ l.support → ↑(ε i) (↑l i • e i) = 0
intro p_not_in
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 : ι
p_not_in : ¬i ∈ l.support
⊢ ↑(ε i) (↑l i • e i) = 0
simp [Finsupp.not_mem_support_iff.1 p_not_in]