`zeta_one`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

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

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 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'
 461
 462/-! ### Additional totient values -/
 463
 464/-- φ(2) = 1. -/
 465theorem totient_two : totient 2 = 1 := by
 466  simp [totient]
 467
 468/-- φ(3) = 2. -/
 469theorem totient_three : totient 3 = 2 := by
 470  native_decide
 471
 472/-- φ(4) = 2. -/
 473theorem totient_four : totient 4 = 2 := by
 474  native_decide
 475
 476/-- φ(5) = 4. -/

papers checked against this theorem

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