coeNat

Mathlib.Data.PNat.Factors

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

English

There is a coercion from PrimeMultiset to Multiset ℕ given by toNatMultiset.

Русский

Существует вложение из PrimeMultiset в Multiset ℕ, задаваемое toNatMultiset.

LaTeX

$$coeNat : PrimeMultiset →+ Multiset ℕ$$

Lean4

instance coeNat : Coe PrimeMultiset (Multiset ℕ) :=
  ⟨toNatMultiset⟩

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

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

Разделы

Аффилиация

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