Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-16 04:11 fb1787b1

View on Github →

feat(analysis/seminorm): Group seminorms (#15594) Multiplicativize the existing add_group_seminorm material.

Estimated changes

deleted theorem add_group_seminorm.ext
deleted theorem add_group_seminorm.le_def
deleted theorem add_group_seminorm.lt_def
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