English
For nonzero a,b, the factorization of gcd(a,b) equals the infimum (min) of the factorization of a and b.
Русский
Для ненулевых a,b факторизация gcd(a,b) равна минимуму факторизаций a и b.
LaTeX
$$$$ (\gcd(a,b)).factorization = a.factorization \inf b.factorization. $$$$
Lean4
theorem factorization_gcd {a b : ℕ} (ha_pos : a ≠ 0) (hb_pos : b ≠ 0) :
(gcd a b).factorization = a.factorization ⊓ b.factorization :=
by
let dfac := a.factorization ⊓ b.factorization
let d := dfac.prod (· ^ ·)
have dfac_prime : ∀ p : ℕ, p ∈ dfac.support → Prime p :=
by
intro p hp
have : p ∈ a.primeFactorsList ∧ p ∈ b.primeFactorsList := by simpa [dfac] using hp
exact prime_of_mem_primeFactorsList this.1
have h1 : d.factorization = dfac := prod_pow_factorization_eq_self dfac_prime
have hd_pos : d ≠ 0 := (factorizationEquiv.invFun ⟨dfac, dfac_prime⟩).2.ne'
suffices d = gcd a b by rwa [← this]
apply gcd_greatest
· rw [← factorization_le_iff_dvd hd_pos ha_pos, h1]
exact inf_le_left
· rw [← factorization_le_iff_dvd hd_pos hb_pos, h1]
exact inf_le_right
· intro e hea heb
rcases Decidable.eq_or_ne e 0 with (rfl | he_pos)
· simp only [zero_dvd_iff] at hea
contradiction
have hea' := (factorization_le_iff_dvd he_pos ha_pos).mpr hea
have heb' := (factorization_le_iff_dvd he_pos hb_pos).mpr heb
simp [dfac, ← factorization_le_iff_dvd he_pos hd_pos, h1, hea', heb']
