case h
R : Type u_3
M : Type u_1
ι : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
i : ι
⊢ ↑(basis h) i = e i
R : Type u_3
M : Type u_1
ι : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
⊢ ↑(basis h) = e
ext i
case h
R : Type u_3
M : Type u_1
ι : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
i : ι
⊢ ↑(basis h).repr (e i) = Finsupp.single i 1
case h
R : Type u_3
M : Type u_1
ι : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
i : ι
⊢ ↑(basis h) i = e i
rw [Basis.apply_eq_iff]
case h.h
R : Type u_3
M : Type u_1
ι : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
i j : ι
⊢ ↑(↑(basis h).repr (e i)) j = ↑(Finsupp.single i 1) j
case h
R : Type u_3
M : Type u_1
ι : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
i : ι
⊢ ↑(basis h).repr (e i) = Finsupp.single i 1
ext j
case h.h
R : Type u_3
M : Type u_1
ι : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
i j : ι
⊢ (if j = i then 1 else 0) = if i = j then 1 else 0
case h.h
R : Type u_3
M : Type u_1
ι : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
i j : ι
⊢ ↑(↑(basis h).repr (e i)) j = ↑(Finsupp.single i 1) j
rw [h.basis_repr_apply, coeffs_apply, h.eval, Finsupp.single_apply]
no goals
case h.h
R : Type u_3
M : Type u_1
ι : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
i j : ι
⊢ (if j = i then 1 else 0) = if i = j then 1 else 0
convert if_congr (eq_comm (a := j) (b := i)) rfl rfl