sum_divisors_filter_squarefree — Mathlib

English

Equivalent expression for the same divisor-sum identity with a different presentation.

Русский

Эквивалентное изложение той же тождества суммы по делителям.

LaTeX

$$$\\sum_{d \\in n.divisors \\;\\&\\; Squarefree(d)} f(d) = \\sum_{i \\in (normalizedFactors(n)).toFinset.powerset} f(i.val.prod)$$$

Lean4

theorem sum_divisors_filter_squarefree {n : ℕ} (h0 : n ≠ 0) {α : Type*} [AddCommMonoid α] {f : ℕ → α} :
    ∑ d ∈ n.divisors with Squarefree d, f d =
      ∑ i ∈ (UniqueFactorizationMonoid.normalizedFactors n).toFinset.powerset, f i.val.prod :=
  by
  rw [Finset.sum_eq_multiset_sum, divisors_filter_squarefree h0, Multiset.map_map, Finset.sum_eq_multiset_sum]
  rfl

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