theorem
proved
totient_five
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 477.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
474 native_decide
475
476/-- φ(5) = 4. -/
477theorem totient_five : totient 5 = 4 := by
478 native_decide
479
480/-- φ(6) = 2. -/
481theorem totient_six : totient 6 = 2 := by
482 native_decide
483
484/-- φ(8) = 4. -/
485theorem totient_eight : totient 8 = 4 := by
486 native_decide
487
488/-- φ(45) = 24. -/
489theorem totient_fortyfive : totient 45 = 24 := by
490 native_decide
491
492/-- φ(360) = 96. -/
493theorem totient_threehundredsixty : totient 360 = 96 := by
494 native_decide
495
496/-! ### Ω and ω at prime powers -/
497
498/-- Ω(p^k) = k for prime p. -/
499theorem bigOmega_prime_pow {p k : ℕ} (hp : Prime p) : bigOmega (p ^ k) = k := by
500 have hp' : Nat.Prime p := (prime_iff p).1 hp
501 cases k with
502 | zero => simp [bigOmega_apply]
503 | succ k => exact ArithmeticFunction.cardFactors_apply_prime_pow hp'
504
505/-- ω(p^k) = 1 for prime p and k ≥ 1. -/
506theorem omega_prime_pow {p k : ℕ} (hp : Prime p) (hk : 0 < k) : omega (p ^ k) = 1 := by
507 have hp' : Nat.Prime p := (prime_iff p).1 hp