Theorem continuous_affine_map.to_const_prod_continuous_linear_map_fst
Modification history
2021-11-12 16:30
src/analysis/normed_space/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.to_const_prod_continuous_linear_map_fstView on Github →