exists_orderOf_eq_prime_pow_iff — Mathlib

English

There exists k with orderOf x = p^k iff there exists m with x^{p^m} = 1.

Русский

Существует k такое, что orderOf(x) = p^k тогда и только тогда, когда существует m, такое что x^{p^m} = 1.

LaTeX

$$\exists k:\mathbb{N}, \operatorname{orderOf}(x) = p^k \quad\iff\quad \exists m:\mathbb{N}, x^{p^m} = 1$$

Lean4

@[to_additive exists_addOrderOf_eq_prime_pow_iff]
theorem exists_orderOf_eq_prime_pow_iff : (∃ k : ℕ, orderOf x = p ^ k) ↔ ∃ m : ℕ, x ^ (p : ℕ) ^ m = 1 :=
  ⟨fun ⟨k, hk⟩ => ⟨k, by rw [← hk, pow_orderOf_eq_one]⟩, fun ⟨_, hm⟩ =>
    by
    obtain ⟨k, _, hk⟩ := (Nat.dvd_prime_pow hp.elim).mp (orderOf_dvd_of_pow_eq_one hm)
    exact ⟨k, hk⟩⟩

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