Commit 2025-03-17 17:38 82322451

View on Github →

refactor(Normed/Group/Quotient): streamline, multiplicativise (#21341)

  • Multiplicativise using the (not so) new GroupNorm API.
  • Deprecate the lemmas about the quotient norm that hold for all norms.
  • Move all remaining lemmas to a single QuotientAddGroup namespace. They were currently scattered across _root_, AddSubgroup and QuotientAddGroup.
  • Follow the naming convention in lemma names.

Estimated changes

modified theorem Ideal.Quotient.norm_mk_le
deleted theorem QuotientAddGroup.norm_mk
added theorem QuotientGroup.norm_mk
modified theorem norm_mk_nonneg
modified theorem norm_mk_zero
modified theorem quotient_norm_mk_le'
modified theorem quotient_norm_mk_le
modified theorem quotient_norm_neg
modified theorem quotient_norm_nonneg
modified theorem quotient_norm_sub_rev
added theorem AddCircle.coe_fract
added theorem Metric.isGLB_infDist
added theorem Metric.le_infDist