exists_ordCompl_eq_one — Mathlib

English

If n is a prime power, there exists a prime p such that ordCompl[p] n = 1.

Русский

Если n — простая степень, существует p, для которого ordCompl[p] n = 1.

LaTeX

$$$\exists p:\mathbb{N},\ p\ prime \land ordCompl[p] n = 1$ for IsPrimePow n.$$

Lean4

theorem exists_ordCompl_eq_one {n : ℕ} (h : IsPrimePow n) : ∃ p : ℕ, p.Prime ∧ ordCompl[p] n = 1 :=
  by
  rcases eq_or_ne n 0 with (rfl | hn0); · cases not_isPrimePow_zero h
  rcases isPrimePow_iff_factorization_eq_single.mp h with ⟨p, k, hk0, h1⟩
  rcases em' p.Prime with (pp | pp)
  · refine absurd ?_ hk0.ne'
    simp [← Nat.factorization_eq_zero_of_non_prime n pp, h1]
  refine ⟨p, pp, ?_⟩
  refine Nat.eq_of_factorization_eq (Nat.ordCompl_pos p hn0).ne' (by simp) fun q => ?_
  rw [Nat.factorization_ordCompl n p, h1]
  simp

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