Mathlib v3 is deprecated. Go to Mathlib v4

Theorem affine_map.smul_linear

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.smul_linearView 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.smul_linearView on Github →