English
In a finite cancellative monoid G, for any n ∈ N, the order of x^n equals orderOf(x) divided by gcd(orderOf(x), n).
Русский
В конечном левоотменяющем моноиде G для любого n ∈ ℕ выполняется orderOf(x^n) = orderOf(x) / gcd(orderOf(x), n).
LaTeX
$$$\operatorname{orderOf}(x^n) = \dfrac{\operatorname{orderOf}(x)}{\gcd(\operatorname{orderOf}(x), n)}$$$
Lean4
/-- This is the same as `orderOf_pow'` and `orderOf_pow''` but with one assumption less which is
automatic in the case of a finite cancellative monoid. -/
@[to_additive /-- This is the same as `addOrderOf_nsmul'` and
`addOrderOf_nsmul` but with one assumption less which is automatic in the case of a
finite cancellative additive monoid. -/
]
theorem orderOf_pow (x : G) : orderOf (x ^ n) = orderOf x / gcd (orderOf x) n :=
(isOfFinOrder_of_finite _).orderOf_pow ..
