Theorem isOfFinOrder_iff_zpow_eq_one

Modification history

2025-04-09 11:53

Mathlib/GroupTheory/OrderOfElement.lean

feat: generalize Mathlib.GroupTheory (#23192) …

Modified isOfFinOrder_iff_zpow_eq_one View on Github →

2024-01-06 09:51

Mathlib/GroupTheory/OrderOfElement.lean

feat: Provide glue between `AddCommGroup` and `Module ℤ` (#9345)

Added isOfFinOrder_iff_zpow_eq_one View on Github →