Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-24 18:34 f5afe205

View on Github →

split(analysis/normed/group/seminorm): Split off analysis.seminorm (#16152) Move group_seminorm and add_group_seminorm to a new file analysis.normed.group.seminorm. Move norm_add_group_seminorm to analysis.normed.group.basic. Remove the nonneg field from add_group_seminorm and group_seminorm because it is redundant.

Estimated changes

added structure add_group_seminorm
added theorem group_seminorm.coe_add
added theorem group_seminorm.coe_sup
added theorem group_seminorm.comp_id
added theorem group_seminorm.div_rev
added theorem group_seminorm.ext
added theorem group_seminorm.le_def
added theorem group_seminorm.lt_def
added structure group_seminorm
deleted structure add_group_seminorm
deleted theorem group_seminorm.add_apply
deleted theorem group_seminorm.add_comp
deleted theorem group_seminorm.coe_add
deleted theorem group_seminorm.coe_comp
deleted theorem group_seminorm.coe_le_coe
deleted theorem group_seminorm.coe_lt_coe
deleted theorem group_seminorm.coe_smul
deleted theorem group_seminorm.coe_sup
deleted theorem group_seminorm.coe_zero
deleted def group_seminorm.comp
deleted theorem group_seminorm.comp_apply
deleted theorem group_seminorm.comp_assoc
deleted theorem group_seminorm.comp_id
deleted theorem group_seminorm.comp_mono
deleted theorem group_seminorm.comp_zero
deleted theorem group_seminorm.div_rev
deleted theorem group_seminorm.ext
deleted theorem group_seminorm.inf_apply
deleted theorem group_seminorm.le_def
deleted theorem group_seminorm.le_insert'
deleted theorem group_seminorm.le_insert
deleted theorem group_seminorm.lt_def
deleted theorem group_seminorm.smul_apply
deleted theorem group_seminorm.smul_sup
deleted theorem group_seminorm.sup_apply
deleted theorem group_seminorm.zero_apply
deleted theorem group_seminorm.zero_comp
deleted structure group_seminorm