of — Mathlib · SciLib

English

There is a canonical way to regard any monoid M as an object of the category MonCat.

Русский

Существует канонический способ рассмотреть любой моид M как объект категории MonCat.

LaTeX

$$$\operatorname{MonCat.of}(M) \text{ is the MonCat-object whose underlying carrier is } M \text{ (i.e. the monoid structure is carried by } M).$$$

Lean4

/-- Construct a bundled `MonCat` from the underlying type and typeclass. -/
@[to_additive /-- Construct a bundled `AddMonCat` from the underlying type and typeclass. -/
    ]
abbrev of (M : Type u) [Monoid M] : MonCat :=
  ⟨M⟩

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