Commit 2026-02-18 13:53 2f9c4948

View on Github →

feat: the normal closure of an empty set is the trivial subgroup (#35029) This is a dependency of a larger PR to formalize finitely presented groups (#34236).

Estimated changes