orderOf_eq_prime_pow — Mathlib

English

If the order is a prime power p^(n+1) and x^p^n ≠ 1 but x^p^(n+1) = 1, then orderOf(x) = p^(n+1).

Русский

Если порядок равен степени простого p^(n+1) и выполняются условия, то orderOf(x) = p^(n+1).

LaTeX

$$¬(x^{p^n} = 1) ∧ (x^{p^{n+1}} = 1) ⇒ \operatorname{orderOf}(x) = p^{n+1}$$

Lean4

@[to_additive addOrderOf_eq_prime_pow]
theorem orderOf_eq_prime_pow (hnot : ¬x ^ p ^ n = 1) (hfin : x ^ p ^ (n + 1) = 1) : orderOf x = p ^ (n + 1) := by
  apply minimalPeriod_eq_prime_pow <;> rwa [isPeriodicPt_mul_iff_pow_eq_one]

Похожие утверждения