theorem
proved
totient_six
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions on GitHub at line 481.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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
508 have hk' : k ≠ 0 := Nat.pos_iff_ne_zero.mp hk
509 simp only [omega]
510 exact ArithmeticFunction.cardDistinctFactors_apply_prime_pow hp' hk'
511