theorem
proved
mobius_isMultiplicative
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions on GitHub at line 166.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
163/-! ### Multiplicativity -/
164
165/-- The Möbius function is multiplicative. -/
166theorem mobius_isMultiplicative : ArithmeticFunction.IsMultiplicative mobius := by
167 simp only [mobius]
168 exact ArithmeticFunction.isMultiplicative_moebius
169
170/-! ### Sigma function (sum of divisors) -/
171
172/-- The sum-of-divisors function σ_k. -/
173abbrev sigma (k : ℕ) : ArithmeticFunction ℕ := ArithmeticFunction.sigma k
174
175@[simp] theorem sigma_def (k : ℕ) : sigma k = ArithmeticFunction.sigma k := rfl
176
177/-- σ_k(n) = ∑ d ∣ n, d^k. -/
178theorem sigma_apply {k n : ℕ} : sigma k n = ∑ d ∈ n.divisors, d ^ k := by
179 simp only [sigma, ArithmeticFunction.sigma_apply]
180
181/-- σ_0(n) = number of divisors of n. -/
182theorem sigma_zero_apply {n : ℕ} : sigma 0 n = n.divisors.card := by
183 simp only [sigma, ArithmeticFunction.sigma_zero_apply]
184
185/-- σ_1(n) = sum of divisors of n. -/
186theorem sigma_one_apply {n : ℕ} : sigma 1 n = ∑ d ∈ n.divisors, d := by
187 simp only [sigma, ArithmeticFunction.sigma_one_apply]
188
189/-- σ_k is multiplicative. -/
190theorem sigma_isMultiplicative (k : ℕ) : ArithmeticFunction.IsMultiplicative (sigma k) := by
191 simp only [sigma]
192 exact ArithmeticFunction.isMultiplicative_sigma
193
194/-- σ_0(p) = 2 for prime p. -/
195theorem sigma_zero_prime {p : ℕ} (hp : Prime p) : sigma 0 p = 2 := by
196 have hp' : Nat.Prime p := (prime_iff p).1 hp