Commit 2022-09-12 13:12 28b23c94

View on Github →

feat(analysis/normed/group/seminorm): Group norms (#16237) Define (additive) group norms, which are group seminorms f such that f x = 0 → x = 0 (resp. f x = 0 → x = 1), along with their hom classes.

Estimated changes

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

added theorem add_group_norm.apply_one

added structure add_group_norm

added theorem add_group_seminorm.apply_one

added theorem group_norm.add_apply

added theorem group_norm.apply_one

added theorem group_norm.coe_add

added theorem group_norm.coe_le_coe

added theorem group_norm.coe_lt_coe

added theorem group_norm.coe_sup

added theorem group_norm.ext

added theorem group_norm.le_def

added theorem group_norm.lt_def

added theorem group_norm.sup_apply

added structure group_norm

added theorem group_seminorm.apply_one

added theorem group_seminorm.mul_bdd_below_range_add

added theorem map_eq_zero_iff_eq_one

added theorem map_ne_zero_iff_ne_one

added theorem map_pos_of_ne_one