coe_coeNatMonoidHom

Mathlib.Data.PNat.Factors

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

English

The canonical coercion to Nat via coeNatMonoidHom coincides with the standard embedding.

Русский

Каноническое вложение через coeNatMonoidHom совпадает с обычным вложением.

LaTeX

$$coe_coeNatMonoidHom : (coeNatMonoidHom : PrimeMultiset → Multiset ℕ) = (↑)$$

Lean4

@[simp]
theorem coe_coeNatMonoidHom : (coeNatMonoidHom : PrimeMultiset → Multiset ℕ) = (↑) :=
  rfl

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

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

Разделы

Аффилиация

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