mathlib3
4ff481ad - feat(group_theory/order_of_element): `order_of_pow_coprime` (#17252)

Commit

3 years ago

feat(group_theory/order_of_element): `order_of_pow_coprime` (#17252) Raising an element to a power coprime to its order does not change its order.

Author

tb65536

Parents