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_groupnormed_add_comm_group
  • semi_normed_groupseminormed_add_comm_group. Elision of the underscore corresponds to seminorm (and to counterbalance the name being sensibly longer).
  • normed_group_homnormed_add_group_hom

Estimated changes

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