Commit 2023-09-21 15:29 f328333d

View on Github →

feat(LinearAlgebra/Multilinear): generalize some defs to Semiring (#7284) Also cleanup FunLike-related code and move code about Semirings to a new section. For linear equivalences, generalization to a Semiring required introducing a new Semiring argument, so that R-linear objects are related by an S-linear equivalence.

Estimated changes

Modified Mathlib/LinearAlgebra/Multilinear/Basic.lean

added def MultilinearMap.coeAddMonoidHom

modified theorem MultilinearMap.coe_injective

added theorem MultilinearMap.coe_sum

modified def MultilinearMap.constLinearEquivOfIsEmpty

modified theorem MultilinearMap.sum_apply

modified structure MultilinearMap

Modified Mathlib/LinearAlgebra/Multilinear/FiniteDimensional.lean