isMultiplicative_moebius — Mathlib

English

The Dirichlet convolution of μ with the zeta function is the identity: μ * ζ = 1.

Русский

Свёртка Дирихле μ и ζ равна единице: μ * ζ = 1.

LaTeX

$$μ * ζ = 1$$

Lean4

@[arith_mult]
theorem isMultiplicative_moebius : IsMultiplicative μ :=
  by
  rw [IsMultiplicative.iff_ne_zero]
  refine ⟨by simp, fun {n m} hn hm hnm => ?_⟩
  simp only [moebius, coe_mk, squarefree_mul hnm, ite_zero_mul_ite_zero, cardFactors_mul hn hm, pow_add]

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