ofHom — Mathlib

English

Typecheck a MonoidHom as a morphism in CommMonCat.

Русский

Приведение MonoidHom к морфизму в CommMonCat через ofHom.

LaTeX

$$$\operatorname{CommMonCat.ofHom}(X\to^* Y) = X \to Y$$$

Lean4

/-- Typecheck a `MonoidHom` as a morphism in `CommMonCat`. -/
@[to_additive /-- Typecheck an `AddMonoidHom` as a morphism in `AddCommMonCat`. -/
    ]
abbrev ofHom {X Y : Type u} [CommMonoid X] [CommMonoid Y] (f : X →* Y) : of X ⟶ of Y :=
  ConcreteCategory.ofHom (C := CommMonCat) f

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