Commit 2025-04-06 22:22 ab33df0d

View on Github →

feat(LinearAlgebra/QuadraticForm/Basis): basis expansion of a quadratic map (#18578) Three lemmas about Quadratic maps applied to:

A finite sum
A linearCombination
The representation of an element wrt a basis

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Sym/Sym2/Finsupp.lean

added theorem Finsupp.coe_sym2Mul

added theorem Finsupp.mem_sym2_support_of_mul_ne_zero

added theorem Finsupp.support_sym2Mul_subset

added theorem Finsupp.sym2Mul_apply_mk

added theorem Finsupp.sym2_support_eq_preimage_support_mul

Modified Mathlib/LinearAlgebra/QuadraticForm/Basic.lean

added theorem QuadraticMap.polarSym2_map_smul

Modified Mathlib/LinearAlgebra/QuadraticForm/Basis.lean

added theorem QuadraticMap.apply_linearCombination'

added theorem QuadraticMap.apply_linearCombination

added theorem QuadraticMap.map_finsuppSum'

added theorem QuadraticMap.map_finsuppSum

added theorem QuadraticMap.sum_polar_sub_repr_sq

added theorem QuadraticMap.sum_repr_sq_add_sum_repr_mul_polar