Theorem Monoid.exp_eq_one_of_subsingleton

Modification history

2024-02-23 11:29

Mathlib/GroupTheory/Exponent.lean

feat(GroupTheory/Exponent): lemmas around Monoid.exponent and Subgroup/Submonoid (#10598) …

Modified Monoid.exp_eq_one_of_subsingleton View on Github →

2023-05-25 14:50

Mathlib/GroupTheory/Exponent.lean

feat: port GroupTheory.Exponent (#4313)

Added Monoid.exp_eq_one_of_subsingleton View on Github →