sigma_one_two_pow_two

formal source

 520
 521/-- Concrete sigma values at small prime powers. -/
 522theorem sigma_one_two_pow_one : sigma 1 (2 ^ 1) = 3 := by native_decide
 523theorem sigma_one_two_pow_two : sigma 1 (2 ^ 2) = 7 := by native_decide
 524theorem sigma_one_two_pow_three : sigma 1 (2 ^ 3) = 15 := by native_decide
 525theorem sigma_one_three_pow_one : sigma 1 (3 ^ 1) = 4 := by native_decide
 526theorem sigma_one_three_pow_two : sigma 1 (3 ^ 2) = 13 := by native_decide
 527theorem sigma_one_five_pow_one : sigma 1 (5 ^ 1) = 6 := by native_decide
 528
 529/-! ### Totient multiplicativity -/
 530
 531/-- Euler's totient function is multiplicative. -/
 532theorem totient_isMultiplicative :
 533    ∀ {m n : ℕ}, Nat.Coprime m n → totient (m * n) = totient m * totient n := by
 534  intro m n h
 535  exact totient_mul_of_coprime h
 536
 537/-! ### Divisors of prime powers -/
 538
 539/-- The divisors of p^k are exactly {p^0, p^1, ..., p^k}. -/
 540theorem divisors_prime_pow {p k : ℕ} (hp : Prime p) :
 541    (p ^ k).divisors = (Finset.range (k + 1)).map ⟨(p ^ ·), Nat.pow_right_injective hp.one_lt⟩ := by
 542  have hp' : Nat.Prime p := (prime_iff p).1 hp
 543  exact Nat.divisors_prime_pow hp' k
 544
 545/-- The number of divisors of p^k is k + 1. -/
 546theorem card_divisors_prime_pow {p k : ℕ} (hp : Prime p) : (p ^ k).divisors.card = k + 1 := by
 547  rw [divisors_prime_pow hp]
 548  simp
 549
 550/-! ### Additional small prime facts -/
 551
 552theorem prime_twentythree : Prime 23 := by decide
 553theorem prime_twentynine : Prime 29 := by decide