prime_pow_succ_dvd_mul — Mathlib

English

If p is prime and p^{i+1} ∣ x y, then p^{i+1} ∣ x or p ∣ y.

Русский

Если p простое и p^{i+1} делит x y, тогда либо p^{i+1} делит x, либо p делит y.

LaTeX

$$$\\forall i:\\, \\mathbb{N},\\; \\operatorname{Prime}(p) \\Rightarrow (p^{i+1} \\mid x y \\Rightarrow p^{i+1} \\mid x \\lor p \\mid y).$$$

Lean4

theorem prime_pow_succ_dvd_mul {M : Type*} [CancelCommMonoidWithZero M] {p x y : M} (h : Prime p) {i : ℕ}
    (hxy : p ^ (i + 1) ∣ x * y) : p ^ (i + 1) ∣ x ∨ p ∣ y :=
  by
  rw [or_iff_not_imp_right]
  exact fun a ↦ Prime.pow_dvd_of_dvd_mul_right h (i + 1) a hxy

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