emultiplicity_pow_self

Mathlib.Data.Nat.Multiplicity

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

← MathLib Explorer

English

For a prime p, emultiplicity p (p^n)! equals the sum over i from 0 to n−1 of p^i.

Русский

Для простого p: emultiplicity p (p^n)! равно сумме p^i с i от 0 до n−1.

LaTeX

$$$ emultiplicity(p, (p^n)!) = \sum_{i=0}^{n-1} p^i $$$

Lean4

theorem emultiplicity_pow_self {p n : ℕ} (hp : p.Prime) : emultiplicity p (p ^ n) = n :=
  _root_.emultiplicity_pow_self hp.ne_zero hp.prime.not_unit n

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

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

Разделы

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

Аффилиация

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