Def QuadraticMap.polarSym2

Modification history

2025-02-10 23:46
Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
refactor(LinearAlgebra/QuadraticForm/Basic): Define the lift of the polar to Sym2 (#21593) …
Added QuadraticMap.polarSym2View on Github →