Theorem QuadraticMap.sum_repr_sq_add_sum_repr_mul_polar

Modification history

2025-04-06 22:22
Mathlib/LinearAlgebra/QuadraticForm/Basis.lean
feat(LinearAlgebra/QuadraticForm/Basis): basis expansion of a quadratic map (#18578) …
Added QuadraticMap.sum_repr_sq_add_sum_repr_mul_polarView on Github →