emultiplicity_factorial_le_div_pred

Mathlib.Data.Nat.Multiplicity

URI: https://scilib.ai/kg/mathlib#Nat.Prime.emultiplicity_factorial_le_div_pred

← MathLib Explorer

English

For a prime p and n, emultiplicity p n! ≤ n/(p − 1).

Русский

Для простого p и n верно: ν_p(n!) ≤ n/(p−1).

LaTeX

$$$ emultiplicity(p, n!) \le (n / (p - 1)) $$$

Lean4

theorem emultiplicity_factorial_le_div_pred {p : ℕ} (hp : p.Prime) (n : ℕ) : emultiplicity p n ! ≤ (n / (p - 1) : ℕ) :=
  by
  rw [hp.emultiplicity_factorial (lt_succ_self _)]
  apply WithTop.coe_mono
  exact Nat.geom_sum_Ico_le hp.two_le _ _

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru