Commit 2026-06-17 00:34 749ea6a3

View on Github →

feat(LinearAlgebra): use Is*Apply for MultilinearMap (#40466)

Estimated changes

Modified Mathlib/FieldTheory/Fixed.lean

Modified Mathlib/FieldTheory/JacobsonNoether.lean

Modified Mathlib/LinearAlgebra/Alternating/DomCoprod.lean

Modified Mathlib/LinearAlgebra/Multilinear/Basic.lean

deleted theorem MultilinearMap.add_apply

deleted def MultilinearMap.coeAddMonoidHom

deleted theorem MultilinearMap.coe_smul

deleted theorem MultilinearMap.coe_sum

deleted theorem MultilinearMap.neg_apply

deleted theorem MultilinearMap.smul_apply

deleted theorem MultilinearMap.sub_apply

deleted theorem MultilinearMap.sum_apply

deleted theorem MultilinearMap.zero_apply

Modified Mathlib/LinearAlgebra/RootSystem/CartanMatrix.lean

Modified Mathlib/LinearAlgebra/TensorPower/Pairing.lean

Modified Mathlib/RingTheory/MatrixPolynomialAlgebra.lean

Modified Mathlib/RingTheory/PicardGroup.lean