instInvertibleNatToArithmeticFunctionZeta

English

The zeta function is invertible under Dirichlet convolution, with Möbius μ as its inverse: μ * ζ = ζ * μ = 1.

Русский

zeta-функция обратима относительно свёртки Дирихле, обратной μ: μ * ζ = ζ * μ = 1.

LaTeX

$$μ * ζ = 1 ∧ ζ * μ = 1$$

Lean4

instance : Invertible (ζ : ArithmeticFunction R) where
  invOf := μ
  invOf_mul_self := coe_moebius_mul_coe_zeta
  mul_invOf_self := coe_zeta_mul_coe_moebius

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