Commit 2026-05-23 13:48 2715441e

View on Github →

refactor(GroupTheory/Torsion): make primaryComponent total (#39484) Change primaryComponent to the IsPGroup-style {g | ∃ k, g ^ p ^ k = 1}, making the definitions total over p : ℕ without requiring [Fact p.Prime].

Estimated changes

Modified Mathlib/GroupTheory/Torsion.lean

added theorem CommGroup.mem_primaryComponent

added theorem CommGroup.mem_primaryComponent_iff_orderOf

modified theorem CommGroup.primaryComponent.isPGroup

added theorem CommMonoid.mem_primaryComponent

added theorem CommMonoid.mem_primaryComponent_iff_orderOf

modified theorem CommMonoid.torsion.isTorsion

modified theorem ExponentExists.isTorsion

modified theorem IsTorsion.subgroup

modified theorem Monoid.not_isTorsion_iff