mathlib3
feat(linear_algebra/multilinear-tensor): Add `multilinear_map.dom_coprod_pi`
#5179
Open

feat(linear_algebra/multilinear-tensor): Add `multilinear_map.dom_coprod_pi` #5179

eric-wieser wants to merge 2 commits into master from eric-wieser/multilinear-tensor
eric-wieser
eric-wieser feat(linear_algebra/multilinear-tensor): Add `multilinear_map.of_tmul`
e22eb054
eric-wieser eric-wieser added maybe-later
eric-wieser eric-wieser added WIP
eric-wieser Merge remote-tracking branch 'origin/master' into eric-wieser/multili…
2a335040
eric-wieser eric-wieser changed the title feat(linear_algebra/multilinear-tensor): Add `multilinear_map.of_tmul` feat(linear_algebra/multilinear-tensor): Add `multilinear_map.dom_congr_pi` 5 years ago
eric-wieser eric-wieser changed the title feat(linear_algebra/multilinear-tensor): Add `multilinear_map.dom_congr_pi` feat(linear_algebra/multilinear-tensor): Add `multilinear_map.dom_coprod_pi` 5 years ago
kim-em kim-em added too-late

Login to write a write a comment.

Login via GitHub

Reviewers
No reviews
Assignees
No one assigned
Labels
Milestone