Mathlib v3 is deprecated. Go to Mathlib v4

Theorem continuous_affine_map.coe_smul

Modification history

2022-02-16 13:36
src/topology/algebra/continuous_affine_map.lean
chore(linear_algebra/affine_space/affine_map,topology/algebra/continuous_affine_map): generalized scalar instances (#11978) …
Modified continuous_affine_map.coe_smulView on Github →
2021-11-12 16:30
src/topology/algebra/continuous_affine_map.lean
feat(analysis/normed_space/continuous_affine_map): isometry from space of continuous affine maps to product of codomain with space of continuous linear maps (#10201) …
Added continuous_affine_map.coe_smulView on Github →