Commit 2021-11-04 15:29 5187a427
View on Github →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.
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.