Commit 2025-02-10 23:46 b77fbf37
View on Github →refactor(LinearAlgebra/QuadraticForm/Basic): Define the lift of the polar to Sym2 (#21593)
Given a function f : M → N (M and N additive commutative groups) QuadraticMap.polar f : M → M → N is always symmetric and so has a lift to Sym2 M → N, which is defined as QuadraticMap.polarSym2 in this PR.
This definition allows the statements of QuadraticMap.map_sum and QuadraticMap.map_sum' to be given in a more pleasing form.
The intention is to use polarSym2 more extensively in #18578.