Commit 2021-12-31 16:13 c4caf0ee

View on Github →

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.

Estimated changes

Modified src/data/equiv/basic.lean

added theorem function.Pi_congr_left'_symm_update

added theorem function.Pi_congr_left'_update

Modified src/linear_algebra/multilinear/basic.lean

added def multilinear_map.dom_dom_congr_linear_equiv'