emultiplicity_self

Mathlib.Data.Nat.Multiplicity

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

English

For a prime p, emultiplicity p (p^n) = n.

Русский

Для простого p: emultiplicity p (p^n) = n.

LaTeX

$$$ emultiplicity(p, p^n) = n $$$

Lean4

theorem emultiplicity_self {p : ℕ} (hp : p.Prime) : emultiplicity p p = 1 :=
  (Nat.finiteMultiplicity_iff.2 ⟨hp.ne_one, hp.pos⟩).emultiplicity_self

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

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

Разделы

Аффилиация

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