mobius

formal source

  21open scoped ArithmeticFunction.omega
  22
  23/-- The Möbius function (as an arithmetic function `ℕ → ℤ`). -/
  24abbrev mobius : ArithmeticFunction ℤ := ArithmeticFunction.moebius
  25
  26@[simp] theorem mobius_def : mobius = ArithmeticFunction.moebius := rfl
  27
  28/-- Möbius at a prime: `μ(p) = -1`. -/
  29theorem mobius_prime {p : ℕ} (hp : Prime p) : (mobius p) = -1 := by
  30  -- Mathlib lemma is `ArithmeticFunction.moebius_apply_prime` with `Nat.Prime`.
  31  have hp' : Nat.Prime p := (prime_iff p).1 hp
  32  simpa [mobius] using (ArithmeticFunction.moebius_apply_prime hp')
  33
  34/-- Möbius at a prime square: `μ(p^2) = 0`. -/
  35theorem mobius_prime_sq {p : ℕ} (hp : Prime p) : (mobius (p ^ 2)) = 0 := by
  36  have hp' : Nat.Prime p := (prime_iff p).1 hp
  37  -- Use the prime-power formula with `k = 2`: `μ(p^2) = if 2 = 1 then -1 else 0 = 0`.
  38  simpa [mobius] using
  39    (ArithmeticFunction.moebius_apply_prime_pow (p := p) (k := 2) hp' (by decide : (2 : ℕ) ≠ 0))
  40
  41/-- If `n` is not squarefree, then `μ n = 0`. -/
  42theorem mobius_eq_zero_of_not_squarefree {n : ℕ} (h : ¬Squarefree n) : mobius n = 0 := by
  43  simpa [mobius] using (ArithmeticFunction.moebius_eq_zero_of_not_squarefree (n := n) h)
  44
  45/-- `μ n ≠ 0` iff `n` is squarefree. -/
  46theorem mobius_ne_zero_iff_squarefree {n : ℕ} : mobius n ≠ 0 ↔ Squarefree n := by
  47  simpa [mobius] using (ArithmeticFunction.moebius_ne_zero_iff_squarefree (n := n))
  48
  49/-- `μ n = 0` iff `n` is not squarefree. -/
  50theorem mobius_eq_zero_iff_not_squarefree {n : ℕ} : mobius n = 0 ↔ ¬Squarefree n := by
  51  -- Negate `μ n ≠ 0 ↔ Squarefree n`.
  52  simpa [not_ne_iff] using (not_congr (mobius_ne_zero_iff_squarefree (n := n)))
  53
  54/-- If `n` is squarefree then `μ n = (-1)^(cardFactors n)`. -/