case h.e'_3.h₁.a
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : _root_.Finite ι
i j : ι
⊢ j = i ↔ i = j
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : _root_.Finite ι
i j : ι
⊢ ↑(↑(dualBasis b) i) (↑b j) = if j = i then 1 else 0
convert b.toDual_apply i j using 2
no goals
case h.e'_3.h₁.a
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : _root_.Finite ι
i j : ι
⊢ j = i ↔ i = j
rw [@eq_comm _ j i]