mem_primeFactorsList_mul_right — Mathlib

English

If p ∈ a.primeFactorsList and b ≠ 0, then p ∈ (a·b).primeFactorsList.

Русский

Если p ∈ a.primeFactorsList и b ≠ 0, то p ∈ (a·b).primeFactorsList.

LaTeX

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

Lean4

/-- If `p` is a prime factor of `b` then `p` is also a prime factor of `a * b` for any `a > 0` -/
theorem mem_primeFactorsList_mul_right {p a b : ℕ} (hpb : p ∈ b.primeFactorsList) (ha : a ≠ 0) :
    p ∈ (a * b).primeFactorsList := by
  rw [mul_comm]
  exact mem_primeFactorsList_mul_left hpb ha

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