Skip to content

Commit

Permalink
chore(Normed/Group/Quotient): streamline, multiplicativise
Browse files Browse the repository at this point in the history 
* 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 naming convention in lemma names.
  • Loading branch information
@YaelDillies
YaelDillies committed Feb 2, 2025
1 parent 3232203 commit 5955272
Show file tree
Hide file tree
Showing 2 changed files with 209 additions and 102 deletions.
Loading

0 comments on commit 5955272

Please sign in to comment.