mathlib3
82b0b30e - refactor(analysis/normed_space/normed_group_hom): generalize to semi_normed_group (#6977)

Commit
4 years ago
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). - [x] depends on: #6910
Parents
Loading