theorem proved term proof

`card_divisors_prime_pow`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 546theorem card_divisors_prime_pow {p k : ℕ} (hp : Prime p) : (p ^ k).divisors.card = k + 1 := by

Term-mode proof.

 547  rw [divisors_prime_pow hp]
 548  simp
 549
 550/-! ### Additional small prime facts -/
 551

Lean names referenced from this declaration's body.

divisors_prime_pow in IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions decl_use
Prime in IndisputableMonolith.NumberTheory.Primes.Basic decl_use