feat(linear_algebra/affine_space/affine_map): decomposition of an affine map between modules as an equiv (#10162)
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.






leanprover-community/mathlib,leanprover-community/mathlib