coeNat_ofPrime

Mathlib.Data.PNat.Factors

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

English

The natural multiset corresponding to a singleton prime multiset is the singleton {p} in ℕ.

Русский

Соответствие конвертации единичного множества простого числа в ℕ дает множестa {p}.

LaTeX

$$coeNat_ofPrime(p) : (ofPrime p : Multiset ℕ) = {(p : ℕ)}$$

Lean4

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

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

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

Разделы

Аффилиация

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