Commit 2022-10-24 21:05 fe67b48e

View on Github →

refactor(analysis/normed/group/basic): generalize (semi)normed_group.induced to monoid_hom_class and add more tools to pull back norm structures (#16255)

Estimated changes

Modified src/analysis/normed/field/basic.lean

added def non_unital_normed_ring.induced

added def non_unital_semi_normed_ring.induced

added theorem norm_one_class.induced

added def normed_comm_ring.induced

added def normed_division_ring.induced

added def normed_field.induced

added def normed_ring.induced

added def semi_normed_comm_ring.induced

added def semi_normed_ring.induced

Modified src/analysis/normed/group/basic.lean

modified def normed_comm_group.induced

modified def normed_group.induced

modified def seminormed_comm_group.induced

modified def seminormed_group.induced

Modified src/analysis/normed_space/basic.lean

added def normed_algebra.induced

added def normed_space.induced

Modified src/topology/continuous_function/zero_at_infty.lean

deleted theorem zero_at_infty_continuous_map.coe_to_bcf_add_monoid_hom

deleted def zero_at_infty_continuous_map.to_bcf_add_monoid_hom