Def MultilinearMap.coeAddMonoidHom

Modification history

2026-06-17 00:34

Mathlib/LinearAlgebra/Multilinear/Basic.lean

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

Deleted MultilinearMap.coeAddMonoidHom View on Github →

2023-09-21 15:29

Mathlib/LinearAlgebra/Multilinear/Basic.lean

feat(LinearAlgebra/Multilinear): generalize some defs to `Semiring` (#7284) …

Added MultilinearMap.coeAddMonoidHom View on Github →