card_divisors_prime_pow

formal source

 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
 571/-- vp 2 (4!) = 3. -/
 572theorem vp_factorial_four_two : vp 2 (Nat.factorial 4) = 3 := by native_decide
 573
 574/-- vp 2 (5!) = 3. -/
 575theorem vp_factorial_five_two : vp 2 (Nat.factorial 5) = 3 := by native_decide
 576