factorization_self

Mathlib.Data.Nat.Factorization.Basic

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

English

The multiplicity of prime p in p is 1.

Русский

Показатель факторизации p по p равен 1.

LaTeX

$$$ p.factorization p = 1 $$$

Lean4

/-- The multiplicity of prime `p` in `p` is `1` -/
theorem factorization_self {p : ℕ} (hp : Prime p) : p.factorization p = 1 := by simp [hp]

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

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

Разделы

Аффилиация

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