`bigOmega_apply`

proved

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions
domain: NumberTheory
line: 78 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions on GitHub at line 78.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  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
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.