Def MultilinearMap.coeAddMonoidHom

Modification history

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 →