moebius — Mathlib

English

The Möbius function μ(n) equals (-1)^{Ω(n)} if n is squarefree, and 0 otherwise.

Русский

Мёбиусовa функция μ(n) равна (-1)^{Ω(n)}, если n квадратно свободно, иначе 0.

LaTeX

$$$$\mu(n) = \begin{cases}(-1)^{\Omega(n)}, & \text{Squarefree}(n); \\ 0, & \text{otherwise.}\end{cases}$$$$

Lean4

/-- `μ` is the Möbius function. If `n` is squarefree with an even number of distinct prime factors,
  `μ n = 1`. If `n` is squarefree with an odd number of distinct prime factors, `μ n = -1`.
  If `n` is not squarefree, `μ n = 0`. -/
def moebius : ArithmeticFunction ℤ :=
  ⟨fun n => if Squarefree n then (-1) ^ cardFactors n else 0, by simp⟩

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