[ add ] `Centre` of a `Group` etc.#2863

Closed

jamesmckinna wants to merge 25 commits intoagda:masterfrom

jamesmckinna:centres

Commits on Nov 6, 2025

Commits on Nov 7, 2025

fix: layout of `record`s
jamesmckinna
committed

Commits on Nov 8, 2025

fix: tighten imports
jamesmckinna
committed

Commits on Nov 9, 2025

refactor: simplify throughout, making clear the relationship with `NormalSubgroup`
jamesmckinna
committed

Commits on Nov 10, 2025

Commits on Nov 11, 2025