theorem
proved
totient_three_pow_two
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 799.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
796
797/-- φ(3^k) values. -/
798theorem totient_three_pow_one : totient (3 ^ 1) = 2 := by native_decide
799theorem totient_three_pow_two : totient (3 ^ 2) = 6 := by native_decide
800
801/-- φ(5^k) values. -/
802theorem totient_five_pow_one : totient (5 ^ 1) = 4 := by native_decide
803theorem totient_five_pow_two : totient (5 ^ 2) = 20 := by native_decide
804
805/-! ### More concrete arithmetic function values -/
806
807/-- Ω(6) = 2 (since 6 = 2 × 3). -/
808theorem bigOmega_six : bigOmega 6 = 2 := by native_decide
809
810/-- ω(6) = 2 (distinct prime factors: 2, 3). -/
811theorem omega_six : omega 6 = 2 := by native_decide
812
813/-- Ω(12) = 3 (since 12 = 2² × 3). -/
814theorem bigOmega_twelve : bigOmega 12 = 3 := by native_decide
815
816/-- ω(12) = 2 (distinct prime factors: 2, 3). -/
817theorem omega_twelve : omega 12 = 2 := by native_decide
818
819/-- Ω(30) = 3 (since 30 = 2 × 3 × 5). -/
820theorem bigOmega_thirty : bigOmega 30 = 3 := by native_decide
821
822/-- ω(30) = 3 (distinct prime factors: 2, 3, 5). -/
823theorem omega_thirty : omega 30 = 3 := by native_decide
824
825/-- μ(6) = 1 (squarefree with 2 prime factors). -/
826theorem mobius_six : mobius 6 = 1 := by native_decide
827
828/-- μ(30) = -1 (squarefree with 3 prime factors). -/
829theorem mobius_thirty : mobius 30 = -1 := by native_decide