Dual basis

Let $(𝑉, ⟨ \cdot, \cdot ⟩)$ be a nondegenerate finite-dimensional quadratic space. Given a basis ${𝑣 𝑖} 𝑛 𝑖 = 1$ , the dual basis is a unique basis defined by #m/def/linalg

⟨ 𝑣' 𝑖, 𝑣 𝑗 ⟩ = 𝛿 𝑖 𝑗

Proof of existence and uniqueness

#missing/proof

#state/develop | #lang/en | #SemBr