omega_def

formal source

  81/-- Number of distinct prime divisors — ω(n). -/
  82abbrev omega : ArithmeticFunction ℕ := ArithmeticFunction.cardDistinctFactors
  83
  84@[simp] theorem omega_def : omega = ArithmeticFunction.cardDistinctFactors := rfl
  85
  86/-- `ω(n) = n.primeFactorsList.dedup.length`. -/
  87theorem omega_apply {n : ℕ} : omega n = n.primeFactorsList.dedup.length := by
  88  simp only [omega, ArithmeticFunction.cardDistinctFactors_apply]
  89
  90/-- For squarefree `n ≠ 0`, `Ω(n) = ω(n)` (all exponents are 1). -/
  91theorem bigOmega_eq_omega_of_squarefree {n : ℕ} (hn : n ≠ 0) (hsq : Squarefree n) :
  92    bigOmega n = omega n := by
  93  simp only [bigOmega, omega]
  94  exact ((ArithmeticFunction.cardDistinctFactors_eq_cardFactors_iff_squarefree hn).mpr hsq).symm
  95
  96/-! ### Euler's totient function φ (via `Nat.totient`) -/
  97
  98/-- Euler's totient function wrapper. -/
  99def totient (n : ℕ) : ℕ := Nat.totient n
 100
 101@[simp] theorem totient_apply {n : ℕ} : totient n = Nat.totient n := rfl
 102
 103/-- φ(1) = 1. -/
 104theorem totient_one : totient 1 = 1 := by
 105  simp [totient, Nat.totient_one]
 106
 107/-- φ(p) = p - 1 for prime p. -/
 108theorem totient_prime {p : ℕ} (hp : Prime p) : totient p = p - 1 := by
 109  have hp' : Nat.Prime p := (prime_iff p).1 hp
 110  simp [totient, Nat.totient_prime hp']
 111
 112/-- φ(p^k) = p^(k-1) * (p - 1) for prime p and k ≥ 1. -/
 113theorem totient_prime_pow {p k : ℕ} (hp : Prime p) (hk : 0 < k) :
 114    totient (p ^ k) = p ^ (k - 1) * (p - 1) := by