Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-24 16:34 d1bd9c5d

View on Github →

chore(*): Rename normed_group to normed_add_comm_group (#15619)

  • normed_group → normed_add_comm_group
  • semi_normed_group → seminormed_add_comm_group. Elision of the underscore corresponds to seminorm (and to counterbalance the name being sensibly longer).
  • normed_group_hom → normed_add_group_hom

Estimated changes

modified structure picard_lindelof
modified theorem asymptotics.is_O_pi
modified theorem asymptotics.is_O_with_pi
modified theorem asymptotics.is_o_pi
modified theorem summable_of_is_O
modified theorem summable_of_is_O_nat
modified theorem asymptotics.is_o.sum_range
modified theorem filter.tendsto.cesaro_smul
modified theorem cont_diff_on.prod_map
modified theorem deriv_within_Ioi_eq_Ici
modified structure cont_diff_bump
modified theorem norm_with_seminorms
modified theorem matrix.frobenius_nnnorm_one
modified theorem nnnorm_norm
modified theorem nnnorm_one
modified theorem norm_norm
modified theorem norm_one_class.nontrivial
modified theorem SemiNormedGroup.coe_of
modified def SemiNormedGroup.of
modified def SemiNormedGroup
modified theorem SemiNormedGroup₁.coe_of
modified def SemiNormedGroup₁.of
modified def SemiNormedGroup₁
modified theorem add_subgroup.coe_norm
modified theorem add_subgroup.norm_coe
modified theorem nnnorm_le_pi_nnnorm
modified theorem norm_le_pi_norm
deleted structure normed_group.core
modified theorem pi.nnnorm_def
modified theorem pi.norm_def
modified theorem pi.sum_norm_apply_le_norm
modified theorem pi_nnnorm_const
modified theorem pi_nnnorm_le_iff
modified theorem pi_nnnorm_lt_iff
modified theorem pi_norm_const
modified theorem pi_norm_le_iff
modified theorem pi_norm_lt_iff
deleted structure semi_normed_group.core
modified theorem exists_pos_bound_of_bound
added structure normed_add_group_hom
deleted theorem normed_group_hom.bound
deleted theorem normed_group_hom.coe_add
deleted theorem normed_group_hom.coe_comp
deleted theorem normed_group_hom.coe_id
deleted theorem normed_group_hom.coe_inj
deleted theorem normed_group_hom.coe_ker
deleted theorem normed_group_hom.coe_mk
deleted theorem normed_group_hom.coe_neg
deleted theorem normed_group_hom.coe_smul
deleted theorem normed_group_hom.coe_sub
deleted theorem normed_group_hom.coe_sum
deleted theorem normed_group_hom.coe_zero
deleted theorem normed_group_hom.ext
deleted theorem normed_group_hom.ext_iff
deleted def normed_group_hom.id
deleted theorem normed_group_hom.ker_zero
deleted theorem normed_group_hom.mem_ker
deleted theorem normed_group_hom.norm_def
deleted theorem normed_group_hom.norm_id
deleted structure normed_group_hom
deleted structure normed_group_hom.is_quotient
deleted theorem normed_group_hom.lift_mk
modified def homeomorph_unit_ball
modified theorem is_equivalent.summable_iff
modified theorem summable_norm_iff
modified theorem summable_of_is_O'
modified theorem summable_of_is_O_nat'
modified theorem summable_of_is_equivalent
modified theorem separate_convex_open_set
modified structure linear_isometry
modified def lp
modified def pre_lp
modified theorem pi_Lp.dist_eq_of_L2
modified theorem pi_Lp.edist_eq_of_L2
modified theorem pi_Lp.nndist_eq_of_L2
modified theorem pi_Lp.nnnorm_eq_of_L2
modified theorem pi_Lp.nnnorm_equiv_symm_one
modified theorem pi_Lp.norm_eq_of_L2
modified theorem pi_Lp.norm_equiv_symm_const
modified theorem pi_Lp.norm_equiv_symm_one
modified theorem tendsto_norm_zero'
modified theorem add_salem_spencer_sphere
modified theorem smooth_map.coe_smul
modified theorem smooth_map.smul_comp'
modified theorem smooth_map.smul_comp
modified def measure_theory.Lp