case h.h
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 : ι
x : M
⊢ ↑(↑(dualBasis b) i) x = ↑(coord b i) x
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 ι
⊢ ↑(dualBasis b) = coord b
ext (i x)
no goals
case h.h
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 : ι
x : M
⊢ ↑(↑(dualBasis b) i) x = ↑(coord b i) x
apply dualBasis_apply