Mathlib v3 is deprecated. Go to Mathlib v4

Def affine_map.to_const_prod_linear_map

Modification history

2022-02-16 13:36
src/linear_algebra/affine_space/affine_map.lean
chore(linear_algebra/affine_space/affine_map,topology/algebra/continuous_affine_map): generalized scalar instances (#11978) …
Modified affine_map.to_const_prod_linear_mapView on Github →
2021-11-04 15:29
src/linear_algebra/affine_space/affine_map.lean
feat(linear_algebra/affine_space/affine_map): decomposition of an affine map between modules as an equiv (#10162) …
Added affine_map.to_const_prod_linear_mapView on Github →