2022-10-24 21:05
src/topology/continuous_function/zero_at_infty.lean
refactor(analysis/normed/group/basic): generalize `(semi)normed_group.induced` to `monoid_hom_class` and add more tools to pull back norm structures (#16255)
Deleted zero_at_infty_continuous_map.to_bcf_add_monoid_hom