English
The sum over squarefree divisors of n equals the sum over the subsets of the multiset of normalized factors of n.
Русский
Сумма по квадратносвободным делителям n равна сумме по подмножествам множества нормализованных факторов n.
LaTeX
$$$\\sum_{d \\in n.divisors\\; \\&\\; Squarefree(d)} f(d) \\\\;= \\\\ \\sum_{i \\in (normalizedFactors(n)).toFinset.powerset} f(i.val.prod)$$$
Lean4
theorem divisors_filter_squarefree {n : ℕ} (h0 : n ≠ 0) :
{d ∈ n.divisors | Squarefree d}.val =
(UniqueFactorizationMonoid.normalizedFactors n).toFinset.powerset.val.map fun x => x.val.prod :=
by
rw [(Finset.nodup _).ext ((Finset.nodup _).map_on _)]
· intro a
simp only [Multiset.mem_filter, Multiset.mem_map, Finset.filter_val, ← Finset.mem_def, mem_divisors]
constructor
· rintro ⟨⟨an, h0⟩, hsq⟩
use (UniqueFactorizationMonoid.normalizedFactors a).toFinset
simp only [Finset.mem_powerset]
rcases an with ⟨b, rfl⟩
rw [mul_ne_zero_iff] at h0
rw [UniqueFactorizationMonoid.squarefree_iff_nodup_normalizedFactors h0.1] at hsq
rw [Multiset.toFinset_subset, Multiset.toFinset_val, hsq.dedup, ← associated_iff_eq,
normalizedFactors_mul h0.1 h0.2]
exact ⟨Multiset.subset_of_le (Multiset.le_add_right _ _), prod_normalizedFactors h0.1⟩
· rintro ⟨s, hs, rfl⟩
rw [Finset.mem_powerset, ← Finset.val_le_iff, Multiset.toFinset_val] at hs
have hs0 : s.val.prod ≠ 0 := by
rw [Ne, Multiset.prod_eq_zero_iff]
intro con
apply
not_irreducible_zero (irreducible_of_normalized_factor 0 (Multiset.mem_dedup.1 (Multiset.mem_of_le hs con)))
rw [(prod_normalizedFactors h0).symm.dvd_iff_dvd_right]
refine ⟨⟨Multiset.prod_dvd_prod_of_le (le_trans hs (Multiset.dedup_le _)), h0⟩, ?_⟩
have h :=
UniqueFactorizationMonoid.factors_unique irreducible_of_normalized_factor
(fun x hx => irreducible_of_normalized_factor x (Multiset.mem_of_le (le_trans hs (Multiset.dedup_le _)) hx))
(prod_normalizedFactors hs0)
rw [associated_eq_eq, Multiset.rel_eq] at h
rw [UniqueFactorizationMonoid.squarefree_iff_nodup_normalizedFactors hs0, h]
apply s.nodup
· intro x hx y hy h
rw [← Finset.val_inj, ← Multiset.rel_eq, ← associated_eq_eq]
rw [← Finset.mem_def, Finset.mem_powerset] at hx hy
apply UniqueFactorizationMonoid.factors_unique _ _ (associated_iff_eq.2 h)
· intro z hz
apply irreducible_of_normalized_factor z
· rw [← Multiset.mem_toFinset]
apply hx hz
· intro z hz
apply irreducible_of_normalized_factor z
· rw [← Multiset.mem_toFinset]
apply hy hz
