mathlib3
b4ce9b7f - feat(group_theory/order_of_element): exists_pow_eq_self_of_coprime (#6875)

Commit

4 years ago

feat(group_theory/order_of_element): exists_pow_eq_self_of_coprime (#6875) If `n` is coprime to the order of `g`, then there exists an `m` such that `(g ^ n) ^ m = g`.

Author

tb65536

Parents

b449a3cd

mathlib3 b4ce9b7f - feat(group_theory/order_of_element): exists_pow_eq_self_of_coprime (#6875)

mathlib3
b4ce9b7f - feat(group_theory/order_of_element): exists_pow_eq_self_of_coprime (#6875)