sum_eq_iff_sum_mul_moebius_eq — Mathlib

English

Möbius inversion for rings: for f,g : ℕ → R with R a non-associative ring, the sum over divisors equals a sum of μ-weighted g-values with multiplication.

Русский

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

LaTeX

$$∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, (μ x.fst : R) * g x.snd = f n$$

Lean4

/-- Möbius inversion for functions to a `Ring`. -/
theorem sum_eq_iff_sum_mul_moebius_eq [NonAssocRing R] {f g : ℕ → R} :
    (∀ n > 0, ∑ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, (μ x.fst : R) * g x.snd = f n :=
  by
  rw [sum_eq_iff_sum_smul_moebius_eq]
  apply forall_congr'
  refine fun a => imp_congr_right fun _ => (sum_congr rfl fun x _hx => ?_).congr_left
  rw [zsmul_eq_mul]

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