mathlib3
5e93545f - feat(linear_algebra/multilinear): Generalize dom_dom_congr for equivalences between types (#5180)

Commit

5 years ago

feat(linear_algebra/multilinear): Generalize dom_dom_congr for equivalences between types (#5180) This also bundles the operation into an equivalence.

Author

eric-wieser

Parents

8da5f23f

mathlib3 5e93545f - feat(linear_algebra/multilinear): Generalize dom_dom_congr for equivalences between types (#5180)

mathlib3
5e93545f - feat(linear_algebra/multilinear): Generalize dom_dom_congr for equivalences between types (#5180)