English
The pair of maps F(n) = support of factorization of n and G(S) = ∏ p ∈ S p realizes a inverse relationship between squarefree naturals and finite sets of primes.
Русский
Пара отображений F(n) = опорa разложения n по простым и G(S) = ∏ p в S p образуют взаимно обратную связь между квадратно свободными натуральными числами и конечными множествами простых чисел.
LaTeX
$$$F(n) := (\\\\text{factorization}(n)).\\\\text{support}, \\\\ G(S) := \\\\prod_{p \\\\in S} p, \\\\text{then } F(n) \\\\text{and } G(S) \text{ form an inverse correspondence between } \\\\{n \\\\mid \\\\operatorname{Squarefree}(n)\\\\} \\\\text{and } \\\\{S \\\\mid \\\\forall p \\\\in S, p.\\\\Prime\\\\}.$$$
Lean4
theorem primeFactors_div_gcd (hm : Squarefree m) (hn : n ≠ 0) :
primeFactors (m / m.gcd n) = primeFactors m \ primeFactors n :=
by
ext p
have : m / m.gcd n ≠ 0 := by simp [gcd_ne_zero_right hn, gcd_le_left _ hm.ne_zero.bot_lt]
simp only [mem_primeFactors, ne_eq, this, not_false_eq_true, and_true, not_and, mem_sdiff, hm.ne_zero, hn,
dvd_div_iff_mul_dvd (gcd_dvd_left _ _)]
refine
⟨fun hp ↦
⟨⟨hp.1, dvd_of_mul_left_dvd hp.2⟩, fun _ hpn ↦
hp.1.not_isUnit <| hm _ <| (mul_dvd_mul_right (dvd_gcd (dvd_of_mul_left_dvd hp.2) hpn) _).trans hp.2⟩,
fun hp ↦ ⟨hp.1.1, Coprime.mul_dvd_of_dvd_of_dvd ?_ (gcd_dvd_left _ _) hp.1.2⟩⟩
rw [coprime_comm, hp.1.1.coprime_iff_not_dvd]
exact fun hpn ↦ hp.2 hp.1.1 <| hpn.trans <| gcd_dvd_right _ _
