Theorem Monoid.minOrder_le_natCard

Modification history

2025-07-27 09:45

Mathlib/GroupTheory/Order/Min.lean

chore: replace `Monoid.IsTorsionFree` with `IsMulTorsionFree` (#24311) …

Modified Monoid.minOrder_le_natCard View on Github →

2023-11-15 15:04

Mathlib/GroupTheory/Order/Min.lean

feat: Minimum torsion of a group (#8411) …

Added Monoid.minOrder_le_natCard View on Github →