mem_primeFactorsList_mul_left — Mathlib

English

For a coprime a,b, p ∈ (a·b).primeFactorsList is equivalent to p ∈ a.primeFactorsList ∪ b.primeFactorsList.

Русский

Для коприм a,b эквивалентно: p ∈ primeFactorsList(a·b) ⇔ p ∈ primeFactorsList(a) ∪ primeFactorsList(b).

LaTeX

$$hab : Coprime a b → ∀ p, p ∈ (a*b).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ b.primeFactorsList$$

Lean4

/-- If `p` is a prime factor of `a` then `p` is also a prime factor of `a * b` for any `b > 0` -/
theorem mem_primeFactorsList_mul_left {p a b : ℕ} (hpa : p ∈ a.primeFactorsList) (hb : b ≠ 0) :
    p ∈ (a * b).primeFactorsList := by
  rcases eq_or_ne a 0 with (rfl | ha)
  · simp at hpa
  apply (mem_primeFactorsList_mul ha hb).2 (Or.inl hpa)

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