commMonoidObj — Mathlib

English

For any j, the object F.obj j in CommMonCat is endowed with a CommMonoid structure (via the forgetful functor to MonCat).

Русский

Для каждого j объект F.obj j в CommMonCat имеет структуру коммутативного моноида (через забывающую функторную связь с MonCat).

LaTeX

$$$\forall j,\; CommMonoid\bigl((F\;\downarrow\;forget\ CommMonCat).obj j\bigr)$$$

Lean4

@[to_additive]
instance commMonoidObj (j) : CommMonoid ((F ⋙ forget CommMonCat.{u}).obj j) :=
  inferInstanceAs <| CommMonoid (F.obj j)

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