coePNat_ofPrime

Mathlib.Data.PNat.Factors

URI: https://scilib.ai/kg/mathlib#PrimeMultiset.coePNat_ofPrime

English

The multiset of PNats corresponding to a prime p is the singleton {p}.

Русский

Мультсет PNats, соответствующий простому p, равен единственному множеству {p}.

LaTeX

$$coePNat_ofPrime(p) : (ofPrime p : Multiset ℕ+) = {(p : ℕ+)}$$

Lean4

theorem coePNat_ofPrime (p : Nat.Primes) : (ofPrime p : Multiset ℕ+) = {(p : ℕ+)} :=
  rfl

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

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

Разделы

Аффилиация

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