emultiplicity_one

Mathlib.Data.Nat.Multiplicity

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

English

For a prime p, the multiplicity of p in 1 is 0.

Русский

Для простого p кратность p в 1 равна 0.

LaTeX

$$$ emultiplicity(p,1) = 0 $$$

Lean4

theorem emultiplicity_one {p : ℕ} (hp : p.Prime) : emultiplicity p 1 = 0 :=
  emultiplicity_of_one_right hp.prime.not_unit

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

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

Разделы

Аффилиация

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