coe_of

Mathlib.Algebra.Category.MonCat.Basic

URI: https://scilib.ai/kg/mathlib#MonCat.coe_of

← MathLib Explorer

English

The type of MonCat.of M is equal to M.

Русский

Тип MonCat.of M равен M.

LaTeX

$$$(MonCat.of\,M:\text{ Type } u) = M$$$

Lean4

@[to_additive]
  -- This is not `simp` to avoid rewriting in types of terms.

theorem coe_of (M : Type u) [Monoid M] : (MonCat.of M : Type u) = M :=
  rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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