Theorem Sym2.lift_comp_map

Modification history

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