English
For a prime p and log p n < b, p^r ∣ n! iff r ≤ ∑ i ∈ Ico 1 b, n / p^i.
Русский
Для простого p и b > log_p n верно: p^r ∣ n! тогда и только тогда, когда r ≤ сумма по i∈Ico(1,b) floor(n/p^i).
LaTeX
$$$ p^r \mid n! \iff r \le \sum_{i \in Ico(1,b)} \left\lfloor \dfrac{n}{p^i} \right\rfloor $$$
Lean4
/-- A prime power divides `n!` iff it is at most the sum of the quotients `n / p ^ i`.
This sum is expressed over the set `Ico 1 b` where `b` is any bound greater than `log p n` -/
theorem pow_dvd_factorial_iff {p : ℕ} {n r b : ℕ} (hp : p.Prime) (hbn : log p n < b) :
p ^ r ∣ n ! ↔ r ≤ ∑ i ∈ Ico 1 b, n / p ^ i := by
rw [← WithTop.coe_le_coe, ENat.some_eq_coe, ← hp.emultiplicity_factorial hbn, pow_dvd_iff_le_emultiplicity]
