divisors_prime_pow

formal source

 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
 563theorem prime_seventythree : Prime 73 := by decide
 564theorem prime_seventynine : Prime 79 := by decide
 565theorem prime_eightythree : Prime 83 := by decide
 566theorem prime_eightynine : Prime 89 := by decide
 567theorem prime_ninetyseven : Prime 97 := by decide
 568
 569/-! ### Factorial valuations (decidable facts) -/
 570