primeFactors_gcd — Mathlib

English

Let a,b > 0. The prime factors of gcd(a,b) are exactly the intersection of the prime factors of a and b.

Русский

Пусть a,b > 0. Простые делители НОД(a,b) равны пересечению простых делителей a и b.

LaTeX

$$$ (a \\neq 0) \\land (b \\neq 0) \\Rightarrow (a \\gcd b).primeFactors = a.primeFactors \\cap b.primeFactors $$$

Lean4

theorem primeFactors_gcd (ha : a ≠ 0) (hb : b ≠ 0) : (a.gcd b).primeFactors = a.primeFactors ∩ b.primeFactors := by ext;
  simp [dvd_gcd_iff, ha, hb, gcd_ne_zero_left ha]; aesop

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