not_dvd_ordCompl — Mathlib

English

For prime p and n ≠ 0, p does not divide ordCompl_p(n).

Русский

Для простого p и n ≠ 0: p не делит ordCompl_p(n).

LaTeX

$$$$ p \text{ prime},\ n \neq 0 \Rightarrow \neg(p \mid \operatorname{ordCompl}_{p}(n)). $$$$

Lean4

theorem not_dvd_ordCompl {n p : ℕ} (hp : Prime p) (hn : n ≠ 0) : ¬p ∣ ordCompl[p] n :=
  by
  rw [Nat.Prime.dvd_iff_one_le_factorization hp (ordCompl_pos p hn).ne']
  rw [Nat.factorization_div (Nat.ordProj_dvd n p)]
  simp [hp.factorization]

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