mu — Mathlib · SciLib

English

There exists a Möbius function μ on IncidenceAlgebra 𝕜 α which inverts zeta; μ acts as the inverse of zeta under convolution.

Русский

Существует функция Мёбиуса μ на IncidenceAlgebra 𝕜 α, которая является обратной к ζ по свёртке, то есть μ является обратной к зета.

LaTeX

$$$ (\mu 𝕜) \star (\zeta 𝕜) = 1 = (\zeta 𝕜) \star (\mu 𝕜) $$$

Lean4

/-- The Möbius function which inverts `zeta` as an element of the incidence algebra. -/
def mu : IncidenceAlgebra 𝕜 α :=
  ⟨muFun 𝕜, fun a b ↦
    not_imp_comm.1 fun h ↦ by
      rw [muFun_apply] at h
      split_ifs at h with hab
      · exact hab.le
      · rw [neg_eq_zero] at h
        obtain ⟨⟨x, hx⟩, -⟩ := exists_ne_zero_of_sum_ne_zero h
        exact (nonempty_Ico.1 ⟨x, hx⟩).le⟩

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