mem_primeFactorsList_mul — Mathlib

English

If a,b > 0, then p is a prime factor of (a·b) iff p is a prime factor of a or of b.

Русский

Если a,b > 0, то p является простым делителем a·b тогда и только тогда, когда p делит a или p делит b.

LaTeX

$$a ≠ 0 → b ≠ 0 → (p ∈ (a*b).primeFactorsList) ↔ (p ∈ a.primeFactorsList ∨ p ∈ b.primeFactorsList)$$

Lean4

theorem mem_primeFactorsList_mul {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) {p : ℕ} :
    p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∨ p ∈ b.primeFactorsList :=
  by
  rw [mem_primeFactorsList (mul_ne_zero ha hb), mem_primeFactorsList ha, mem_primeFactorsList hb, ← and_or_left]
  simpa only [and_congr_right_iff] using Prime.dvd_mul

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