Code

feat: group markings#19475

Code

Open

YaelDillies wants to merge 4 commits intomasterleanprover-community/mathlib4:masterfrom group_markingleanprover-community/mathlib4:group_markingCopy head branch name to clipboard

+436-165

Commits

Commits on Feb 3, 2025

• chore(Normed/Group/Quotient): streamline, multiplicativise

  Show description for 1278b3a
  YaelDillies

  committed
  1278b3a

  Copy full SHA for 1278b3a

• refactor(Normed/Group/Quotient): generalise to non-commutative groups

  Show description for a15587b
  YaelDillies

  committed
  a15587b

  Copy full SHA for a15587b

• feat: group markings

  Show description for ac294fa
  YaelDillies

  committed
  ac294fa

  Copy full SHA for ac294fa

• wip

  YaelDillies

  committed
  75a713a

  Copy full SHA for 75a713a