exists_ordCompl_eq_one_iff_isPrimePow

English

For n ≠ 1, IsPrimePow n iff there exists p with ordCompl[p] n = 1 and p prime.

Русский

Для n ≠ 1, IsPrimePow n эквивалентно существованию p, для которого ordCompl[p] n = 1 и p — простое.

LaTeX

$$$n \neq 1 \Rightarrow IsPrimePow(n) \iff \exists p: \mathbb{N}, (p\ prime \land ordCompl[p] n = 1).$$$

Lean4

theorem exists_ordCompl_eq_one_iff_isPrimePow {n : ℕ} (hn : n ≠ 1) :
    IsPrimePow n ↔ ∃ p : ℕ, p.Prime ∧ ordCompl[p] n = 1 :=
  by
  refine ⟨fun h => IsPrimePow.exists_ordCompl_eq_one h, fun h => ?_⟩
  rcases h with ⟨p, pp, h⟩
  rw [isPrimePow_nat_iff]
  rw [← Nat.eq_of_dvd_of_div_eq_one (Nat.ordProj_dvd n p) h] at hn ⊢
  refine ⟨p, n.factorization p, pp, ?_, by simp⟩
  contrapose! hn
  simp [Nat.le_zero.1 hn]

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