Commit 2021-04-06 09:41 82b0b30e

View on Github →

refactor(analysis/normed_space/normed_group_hom): generalize to semi_normed_group (#6977) This is part of a series of PR to have the theory of semi_normed_group (and related concepts) in mathlib. We generalize here normed_group_hom to semi_normed_group (keeping the old name to avoid too long names).

depends on: #6910

Estimated changes

Modified src/analysis/normed_space/normed_group_hom.lean

modified theorem exists_pos_bound_of_bound

modified theorem normed_group_hom.norm_id

added theorem normed_group_hom.norm_id_of_nontrivial_seminorm

added theorem normed_group_hom.op_norm_zero

modified theorem normed_group_hom.op_norm_zero_iff

modified structure normed_group_hom