Commit 2026-07-31 14:37 ce88332a

View on Github →

feat(LinearAlgebra): use IsApply for QuadraticMap (#42134)

Estimated changes

Modified Counterexamples/CliffordAlgebraNotInjective.lean

Modified Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean

Modified Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean

Modified Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/Basic.lean

deleted theorem QuadraticMap.add_apply

deleted def QuadraticMap.coeFnAddMonoidHom

deleted theorem QuadraticMap.coeFn_add

deleted theorem QuadraticMap.coeFn_neg

deleted theorem QuadraticMap.coeFn_smul

deleted theorem QuadraticMap.coeFn_sub

deleted theorem QuadraticMap.coeFn_sum

deleted theorem QuadraticMap.coeFn_zero

deleted theorem QuadraticMap.neg_apply

deleted theorem QuadraticMap.smul_apply

deleted theorem QuadraticMap.sub_apply

deleted theorem QuadraticMap.sum_apply

deleted theorem QuadraticMap.zero_apply

Modified Mathlib/LinearAlgebra/QuadraticForm/Dual.lean