pow_succ_factorization_not_dvd — Mathlib

English

If n ≠ 0 and p is prime, then p^(n.factorization p + 1) does not divide n.

Русский

Если n ≠ 0 и p — простое, то p^(n.factorization p + 1) не делит n.

LaTeX

$$$n \\neq 0, \\; \\text{Prime}(p) \\Rightarrow \\neg p^{(n.factorization(p) + 1)} \\mid n$$$

Lean4

theorem pow_succ_factorization_not_dvd {n p : ℕ} (hn : n ≠ 0) (hp : p.Prime) : ¬p ^ (n.factorization p + 1) ∣ n :=
  by
  intro h
  rw [← factorization_le_iff_dvd (pow_ne_zero _ hp.ne_zero) hn] at h
  simpa [hp.factorization] using h p

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