affine_map): decomposition of an affine map between modules as an equiv (#10162)

Commit

4 years ago

feat(linear_algebra/affine_space/affine_map): decomposition of an affine map between modules as an equiv (#10162) Formalized as part of the Sphere Eversion project.

Author

ocfnash

Parents

22ec295c

mathlib3 5187a427 - feat(linear_algebra/affine_space/affine_map): decomposition of an affine map between modules as an equiv (#10162)

mathlib3
5187a427 - feat(linear_algebra/affine_space/affine_map): decomposition of an affine map between modules as an equiv (#10162)