totient_two_pow_three

formal source

 791/-- φ(2^k) = 2^k - 2^(k-1) = 2^(k-1) for k ≥ 1 (concrete). -/
 792theorem totient_two_pow_one : totient (2 ^ 1) = 1 := by native_decide
 793theorem totient_two_pow_two : totient (2 ^ 2) = 2 := by native_decide
 794theorem totient_two_pow_three : totient (2 ^ 3) = 4 := by native_decide
 795theorem totient_two_pow_four : totient (2 ^ 4) = 8 := by native_decide
 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