theorem
proved
mobius_one
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions on GitHub at line 430.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
427/-! ### Values at 1 -/
428
429/-- μ(1) = 1. -/
430theorem mobius_one : mobius 1 = 1 := by
431 simp [mobius]
432
433/-- ω(1) = 0. -/
434theorem omega_one : omega 1 = 0 := by
435 simp [omega_apply]
436
437/-- Ω(1) = 0. -/
438theorem bigOmega_one : bigOmega 1 = 0 := by
439 simp [bigOmega_apply]
440
441/-- σ_k(1) = 1 for any k. -/
442theorem sigma_one {k : ℕ} : sigma k 1 = 1 := by
443 simp [sigma_apply]
444
445/-- ζ(1) = 1. -/
446theorem zeta_one : zeta 1 = 1 := by
447 exact zeta_apply (by decide)
448
449/-! ### Values at primes -/
450
451/-- ω(p) = 1 for prime p. -/
452theorem omega_prime {p : ℕ} (hp : Prime p) : omega p = 1 := by
453 have hp' : Nat.Prime p := (prime_iff p).1 hp
454 simp only [omega]
455 exact ArithmeticFunction.cardDistinctFactors_apply_prime hp'
456
457/-- Ω(p) = 1 for prime p. -/
458theorem bigOmega_prime {p : ℕ} (hp : Prime p) : bigOmega p = 1 := by
459 have hp' : Nat.Prime p := (prime_iff p).1 hp
460 exact ArithmeticFunction.cardFactors_apply_prime hp'