primeFactors

Mathlib.Data.Nat.PrimeFin

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

English

If p is prime, then the prime factors of p are exactly {p}.

Русский

Если p простое, то простые делители p равны {p}.

LaTeX

$$$ \\operatorname{primeFactors}(p) = \\{ p \\}$$$

Lean4

@[simp]
protected theorem primeFactors (hp : p.Prime) : p.primeFactors = { p } := by
  simp [Nat.primeFactors, primeFactorsList_prime hp]

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

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

Разделы

Аффилиация

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