Mathlib v3 is deprecated. Go to Mathlib v4

Def continuous_affine_map.to_const_prod_continuous_linear_map

Modification history

2022-03-11 23:40
src/analysis/normed_space/continuous_affine_map.lean
chore(*): update to 3.41.0c (#12591)
Added continuous_affine_map.to_const_prod_continuous_linear_mapView on Github →