pairwise_primeFactors_isRelPrime — Mathlib

English

The pairwise prime factors of a are pairwise relatively prime.

Русский

Парные простые множители a попарно взаимно просты.

LaTeX

$$$$ Set.Pairwise( primeFactors(a) : Set M ) IsRelPrime $$$$

Lean4

theorem pairwise_primeFactors_isRelPrime : Set.Pairwise (primeFactors a : Set M) IsRelPrime :=
  by
  obtain rfl | ha₀ := eq_or_ne a 0
  · simp
  intro x hx y hy hxy
  simp only [Finset.mem_coe, mem_primeFactors, mem_normalizedFactors_iff' ha₀] at hx hy
  rw [hx.1.isRelPrime_iff_not_dvd]
  contrapose! hxy
  have : Associated x y := hx.1.associated_of_dvd hy.1 hxy
  exact this.eq_of_normalized hx.2.1 hy.2.1

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