hasCoe

Mathlib.Data.Sym.Basic

URI: https://scilib.ai/kg/mathlib#Sym.hasCoe

English

There is a canonical coercion from Sym α n to Multiset α given by toMultiset.

Русский

Существует каноническое встраивание из Sym α n в Multiset α через toMultiset.

LaTeX

$$$\\text{Sym.hasCoe}: \\mathrm{Sym}\\;\\alpha\\;n \\hookrightarrow \\mathrm{Multiset}\\;\\alpha\\quad\\text{via }\\mathrm{toMultiset}$$$

Lean4

instance hasCoe (α : Type*) (n : ℕ) : CoeOut (Sym α n) (Multiset α) :=
  ⟨Sym.toMultiset⟩

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

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

Разделы

Аффилиация

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