zeta_mul_mu — Mathlib

English

A dual Möbius inversion: if the hypothesis holds in the dual order, a corresponding inversion formula holds with the dual Möbius function μ on αᵒᵈ.

Русский

Дуальная инверсия Мёбиуса: если гипотеза справедлива в двойственном порядке, то соответствующая формула инверсии сохраняется с дуальным μ на αᵒᵈ.

LaTeX

$$$ moebius\_inversion\_bot(f,g,h) \Rightarrow f x = \sum_{y \le x} μ y x g y $$$

Lean4

theorem zeta_mul_mu [DecidableLE α] : (zeta 𝕜 * mu 𝕜 : IncidenceAlgebra 𝕜 α) = 1 := by rw [mu_eq_mu', zeta_mul_mu']

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