prod_eq_iff_prod_pow_moebius_eq — Mathlib

English

Möbius inversion for functions to a commutative group: the equivalence with product over divisors and μ-powers holds.

Русский

Обратимость Мёбиуса для функций в коммутативной группе: эквивалентности через произведения и μ-возводения в степень.

LaTeX

$$∀ {R} [CommGroup R] {f g : ℕ → R}, (∀ n > 0, ∏ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, ∏ x ∈ n.divisorsAntidiagonal, g x.snd ^ μ x.fst = f n$$

Lean4

/-- Möbius inversion for functions to a `CommGroup`. -/
theorem prod_eq_iff_prod_pow_moebius_eq [CommGroup R] {f g : ℕ → R} :
    (∀ n > 0, ∏ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, ∏ x ∈ n.divisorsAntidiagonal, g x.snd ^ μ x.fst = f n :=
  @sum_eq_iff_sum_smul_moebius_eq (Additive R) _ _ _

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