mem_primeFactorsList_mul_of_coprime

English

For coprime a,b, p is in (a·b).primeFactorsList iff p is in a.primeFactorsList ∪ b.primeFactorsList.

Русский

Для коприм а, b, p принадлежит (a·b).primeFactorsList тогда и только тогда, когда p принадлежит a.primeFactorsList или b.primeFactorsList.

LaTeX

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

Lean4

theorem mem_primeFactorsList_mul_of_coprime {a b : ℕ} (hab : Coprime a b) (p : ℕ) :
    p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ b.primeFactorsList :=
  by
  rcases a.eq_zero_or_pos with (rfl | ha)
  · simp [(coprime_zero_left _).mp hab]
  rcases b.eq_zero_or_pos with (rfl | hb)
  · simp [(coprime_zero_right _).mp hab]
  rw [mem_primeFactorsList_mul ha.ne' hb.ne', List.mem_union_iff]

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