card_divisors_prime_pow
plain-language theorem explainer
The theorem asserts that if p is prime and k a natural number then p^k has exactly k+1 positive divisors. Number theorists preparing multiplicative functions or Möbius inversion steps would cite this when handling prime-power cases. The proof rewrites the divisor set via the explicit range construction in the companion lemma and lets simplification obtain the cardinality.
Claim. If $p$ is prime and $k$ is a natural number, then the set of positive divisors of $p^k$ has cardinality $k+1$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function, to keep statements minimal before layering Dirichlet algebra and inversion. Prime is the transparent alias for Nat.Prime. The immediate upstream result states that the divisors of p^k are exactly the image of the range 0 to k under the map sending i to p^i.
proof idea
The proof is a one-line wrapper that applies the divisors_prime_pow lemma to replace the divisor set with the explicit range image, after which simp computes the cardinality of that finite set.
why it matters
This supplies the standard divisor count for prime powers required by multiplicative arithmetic functions in the same module. It fills the elementary fact needed before Möbius inversion or Dirichlet series can be developed. No downstream uses appear yet, leaving open its precise role in larger Recognition Science constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.