Mathlib v3 is deprecated. Go to Mathlib v4

Def multilinear_map.dom_coprod

Modification history

2021-09-24 11:04
src/linear_algebra/multilinear/basic.lean
chore(algebra/basic): split out facts about lmul (#9300)
Modified multilinear_map.dom_coprodView on Github →
2020-12-04 15:57
src/linear_algebra/multilinear.lean
feat(linear_algebra/multilinear): Add `multilinear_map.coprod` (#5182)
Added multilinear_map.dom_coprodView on Github →