Commit 2024-10-14 12:17 d839ff4a

View on Github →

feat(OrderOfElement): add isOfFinOrder_pow (#17636) Also add IsOfFinOrder.of_pow and a missing @[to_additive].

Estimated changes

Modified Mathlib/GroupTheory/OrderOfElement.lean

added theorem IsOfFinOrder.of_pow

added theorem IsOfFinOrder.one

deleted theorem isOfFinOrder_one

added theorem isOfFinOrder_pow

Modified Mathlib/GroupTheory/Torsion.lean