Mathlib v3 is deprecated. Go to Mathlib v4

Def locally_constant.to_continuous_map_monoid_hom

Modification history

2021-09-22 07:37
src/analysis/normed_space/basic.lean
chore(*): removing unneeded imports (#9278)
Modified locally_constant.to_continuous_map_monoid_homView on Github →
2021-07-28 17:10
src/analysis/normed_space/basic.lean
feat(analysis/normed_space/basic): define inclusion `locally_constant X G → C(X, G)` as various types of bundled morphism (#8448)
Added locally_constant.to_continuous_map_monoid_homView on Github →