Commit 2026-10-05 15:02 ff9a7c19

View on Github →

feat(LinearAlgebra): use IsApply for AlternatingMap (#42140)

Estimated changes

Modified Mathlib/LinearAlgebra/Alternating/Basic.lean

deleted theorem AlternatingMap.add_apply

deleted theorem AlternatingMap.coeFn_smul

deleted theorem AlternatingMap.coe_add

deleted theorem AlternatingMap.coe_neg

deleted theorem AlternatingMap.coe_smul

deleted theorem AlternatingMap.coe_sub

deleted theorem AlternatingMap.coe_zero

deleted theorem AlternatingMap.neg_apply

deleted theorem AlternatingMap.smul_apply

deleted theorem AlternatingMap.sub_apply

added theorem AlternatingMap.toMultilinearMap_add

added theorem AlternatingMap.toMultilinearMap_neg

added theorem AlternatingMap.toMultilinearMap_smul

added theorem AlternatingMap.toMultilinearMap_sub

added theorem AlternatingMap.toMultilinearMap_zero

deleted theorem AlternatingMap.zero_apply

Modified Mathlib/LinearAlgebra/Alternating/DomCoprod.lean

Modified Mathlib/LinearAlgebra/Determinant.lean

Modified Mathlib/LinearAlgebra/Orientation.lean

Modified Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean