Theorem QuadraticMap.polarSym2_sym2Mk

Modification history

2026-02-16 15:42
Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
refactor(Data/Sym/Sym2): curry `mk` (#34803) …
Modified QuadraticMap.polarSym2_sym2MkView on Github →
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.polarSym2_sym2MkView on Github →