card_divisors — Mathlib

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

Похожие утверждения