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⟩