totient_pos

formal source

 784/-! ### Totient product formula helpers -/
 785
 786/-- φ(n) > 0 for n > 0 (strengthened). -/
 787theorem totient_pos {n : ℕ} (hn : 0 < n) : 0 < totient n := by
 788  simp only [totient]
 789  exact Nat.totient_pos.mpr hn
 790
 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