Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-27 03:05 99c23eaf

View on Github →

refactor(analysis/normed_space/basic): add semi_normed_group (#6888) This is part of a series of PR to have semi_normed_group (and related concepts) in mathlib.

To keep the PR as small as possibile I just added the new class semi_normed_group. I didn't introduce anything like semi_normed_ring and I didn't do anything about morphisms.

Estimated changes

modified theorem has_fderiv_at_fst
modified theorem has_fderiv_at_snd
modified theorem has_strict_fderiv_at_fst
modified theorem has_strict_fderiv_at_snd
modified theorem coe_norm_subgroup
modified theorem lipschitz_with.add
modified theorem lipschitz_with.neg
modified theorem lipschitz_with.sub
added theorem ne_zero_of_norm_pos
modified theorem norm_zero
added theorem pi_nnsemi_norm_const
added theorem pi_semi_norm_const
added theorem pi_semi_norm_le_iff
added theorem pi_semi_norm_lt_iff
added theorem prod.nnsemi_norm_def
added theorem prod.semi_norm_def
deleted theorem real.fpow_bit0_norm
deleted theorem real.fpow_even_norm
deleted theorem real.pow_bit0_norm
deleted theorem real.pow_even_norm
added theorem semi_norm_fst_le
added theorem semi_norm_le_pi_norm
added theorem semi_norm_prod_le_iff
added theorem semi_norm_snd_le
added structure semi_normed_group.core