basic): add dependent version of `multilinear_map.dom_dom_congr_linear_equiv` (#10474)

Commit

4 years ago

feat(linear_algebra/multilinear/basic): add dependent version of `multilinear_map.dom_dom_congr_linear_equiv` (#10474) Formalized as part of the Sphere Eversion project.

Author

ocfnash

Parents

9a38c196

mathlib c4caf0ee - feat(linear_algebra/multilinear/basic): add dependent version of `multilinear_map.dom_dom_congr_linear_equiv` (#10474)

mathlib
c4caf0ee - feat(linear_algebra/multilinear/basic): add dependent version of `multilinear_map.dom_dom_congr_linear_equiv` (#10474)