mobius_eq_zero_iff_not_squarefree

formal source

  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)`. -/
  55theorem mobius_apply_of_squarefree {n : ℕ} (hn : Squarefree n) :
  56    mobius n = (-1) ^ ArithmeticFunction.cardFactors n := by
  57  simpa [mobius] using (ArithmeticFunction.moebius_apply_of_squarefree (n := n) hn)
  58
  59/-- A useful bridge: for `n ≠ 0`, `μ n ≠ 0` iff all prime exponents are ≤ 1. -/
  60theorem mobius_ne_zero_iff_vp_le_one {n : ℕ} (hn : n ≠ 0) :
  61    mobius n ≠ 0 ↔ ∀ p : ℕ, vp p n ≤ 1 := by
  62  constructor
  63  · intro hμ
  64    have hsq : Squarefree n := (mobius_ne_zero_iff_squarefree (n := n)).1 hμ
  65    exact (squarefree_iff_vp_le_one (n := n) hn).1 hsq
  66  · intro hvp
  67    have hsq : Squarefree n := (squarefree_iff_vp_le_one (n := n) hn).2 hvp
  68    exact (mobius_ne_zero_iff_squarefree (n := n)).2 hsq
  69
  70/-! ### Additional arithmetic function wrappers -/
  71
  72/-- Number of prime factors (with multiplicity) — Ω(n). -/
  73abbrev bigOmega : ArithmeticFunction ℕ := ArithmeticFunction.cardFactors
  74
  75@[simp] theorem bigOmega_def : bigOmega = ArithmeticFunction.cardFactors := rfl
  76
  77/-- `Ω(n) = n.primeFactorsList.length`. -/
  78theorem bigOmega_apply {n : ℕ} : bigOmega n = n.primeFactorsList.length := by
  79  simp only [bigOmega, ArithmeticFunction.cardFactors_apply]
  80