Theorem QuadraticMap.apply_linearCombination'

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.apply_linearCombination'View on Github →