instCoeTCOrderMonoidHomOfOrderHomClassOfMonoidHomClass

English

There is a canonical coercion from OrderHomClass to OrderMonoidHom via a defined instance.

Русский

Существует каноническое приведение из OrderHomClass к OrderMonoidHom через заданный экземпляр.

LaTeX

$$$\text{OrderMonoidHom}(F, \alpha, \beta)$$$

Lean4

/-- Any type satisfying `OrderMonoidHomClass` can be cast into `OrderMonoidHom` via
  `OrderMonoidHomClass.toOrderMonoidHom`. -/
@[to_additive /-- Any type satisfying `OrderAddMonoidHomClass` can be cast into `OrderAddMonoidHom`
      via `OrderAddMonoidHomClass.toOrderAddMonoidHom`. -/
    ]
instance [OrderHomClass F α β] [MonoidHomClass F α β] : CoeTC F (α →*o β) :=
  ⟨OrderMonoidHomClass.toOrderMonoidHom⟩

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