totient_isMultiplicative

formal source

 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
 554theorem prime_thirtyone : Prime 31 := by decide
 555theorem prime_fortyone : Prime 41 := by decide
 556theorem prime_fortythree : Prime 43 := by decide
 557theorem prime_fortyseven : Prime 47 := by decide
 558theorem prime_fiftythree : Prime 53 := by decide
 559theorem prime_fiftynine : Prime 59 := by decide
 560theorem prime_sixtyone : Prime 61 := by decide
 561theorem prime_sixtyseven : Prime 67 := by decide
 562theorem prime_seventyone : Prime 71 := by decide