Commit 2023-11-10 10:42 1d775649

View on Github →

feat: Simple results about ZMod (#8205)

Estimated changes

Modified Mathlib/Data/ZMod/Defs.lean

Modified Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

Modified Mathlib/GroupTheory/Torsion.lean

added theorem Monoid.isTorsionFree_of_subsingleton