English
Instance providing NonnegHomClass from Group and LinearOrder assumptions.
Русский
Экземпляр, задающий NonnegHomClass из предположений про группу и линейный порядок.
LaTeX
$$$NonnegHomClass(F, \alpha, \beta)$$$
Lean4
/-- Turn an element of a type `F` satisfying `OrderHomClass F α β` and `MonoidHomClass F α β`
into an actual `OrderMonoidHom`. This is declared as the default coercion from `F` to `α →*o β`. -/
@[to_additive (attr := coe) /--
Turn an element of a type `F` satisfying `OrderHomClass F α β` and `AddMonoidHomClass F α β`
into an actual `OrderAddMonoidHom`.
This is declared as the default coercion from `F` to `α →+o β`. -/
]
def toOrderMonoidHom [OrderHomClass F α β] [MonoidHomClass F α β] (f : F) : α →*o β :=
{ (f : α →* β) with monotone' := OrderHomClass.monotone f }
