Theorem isOfFinOrder_iff_zpow_eq_one

Modification history

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 →