sigma_mul_of_coprime

formal source

 766/-! ### Sigma multiplicativity helpers -/
 767
 768/-- σ_k(mn) = σ_k(m) × σ_k(n) for coprime m, n. -/
 769theorem sigma_mul_of_coprime {k m n : ℕ} (h : Nat.Coprime m n) :
 770    sigma k (m * n) = sigma k m * sigma k n := by
 771  simp only [sigma]
 772  exact ArithmeticFunction.isMultiplicative_sigma.map_mul_of_coprime h
 773
 774/-- σ_0(mn) = σ_0(m) × σ_0(n) for coprime m, n. -/
 775theorem sigma_zero_mul_of_coprime {m n : ℕ} (h : Nat.Coprime m n) :
 776    sigma 0 (m * n) = sigma 0 m * sigma 0 n :=
 777  sigma_mul_of_coprime h
 778
 779/-- σ_1(mn) = σ_1(m) × σ_1(n) for coprime m, n. -/
 780theorem sigma_one_mul_of_coprime {m n : ℕ} (h : Nat.Coprime m n) :
 781    sigma 1 (m * n) = sigma 1 m * sigma 1 n :=
 782  sigma_mul_of_coprime h
 783
 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