English
Let n ∈ ℕ be squarefree and t ⊆ n.primeFactors. Then ∏ a ∈ (n.primeFactors \\ t), a = n / ∏ a ∈ t, a.
Русский
Пусть n ∈ ℕ квадратно свободно и t ⊆ n.primeFactors. Тогда ∏ a ∈ (n.primeFactors \\ t), a = n / ∏ a ∈ t, a.
LaTeX
$$$\\\\forall n \\\\in \\\\mathbb N, \\\\operatorname{Squarefree}(n) \\\\Rightarrow \\\\forall t \\\\subseteq n.\\\\primeFactors, \\\\prod_{a \\\\in (n.\\\\primeFactors\\\\setminus t)} a \\\\;=\\\\; \\\\frac{n}{\\\\prod_{a \\\\in t} a}.$$$
Lean4
theorem prod_primeFactors_sdiff_of_squarefree {n : ℕ} (hn : Squarefree n) {t : Finset ℕ} (ht : t ⊆ n.primeFactors) :
∏ a ∈ (n.primeFactors \ t), a = n / ∏ a ∈ t, a :=
by
refine
symm <|
Nat.div_eq_of_eq_mul_left
(Finset.prod_pos fun p hp => (prime_of_mem_primeFactorsList (List.mem_toFinset.mp (ht hp))).pos) ?_
rw [Finset.prod_sdiff ht, prod_primeFactors_of_squarefree hn]
