English
For n ≠ 0, the number of divisors equals the product over prime factors p_i^{e_i} of (e_i + 1).
Русский
Для n ≠ 0 число делителей равно произведению (e_i + 1) по всем простым p_i^{e_i}, составляющим n.
LaTeX
$$$ #n.divisors = \prod_i (e_i + 1) \quad\text{where } n = \prod_i p_i^{e_i} $$$
Lean4
theorem _root_.Nat.card_divisors {n : ℕ} (hn : n ≠ 0) : #n.divisors = n.primeFactors.prod (n.factorization · + 1) :=
by
rw [← sigma_zero_apply, isMultiplicative_sigma.multiplicative_factorization _ hn]
exact
Finset.prod_congr n.support_factorization fun _ h => sigma_zero_apply_prime_pow <| Nat.prime_of_mem_primeFactors h