emultiplicity_pow

Mathlib.Data.Nat.Multiplicity

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

English

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

Русский

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

LaTeX

$$$ emultiplicity(p, m^n) = n \cdot emultiplicity(p,m) $$$

Lean4

theorem emultiplicity_pow {p m n : ℕ} (hp : p.Prime) : emultiplicity p (m ^ n) = n * emultiplicity p m :=
  _root_.emultiplicity_pow hp.prime

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

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

Разделы

Аффилиация

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