English
A structure F that satisfies both OrderHomClass and RingHomClass can be coerced to an actual OrderRingHom; this is the default coercion from F to α →+*o β.
Русский
Любая структура F, удовлетворяющая OrderHomClass и RingHomClass, может быть приведена к настоящему OrderRingHom; это стандартное приведение из F в α →+*o β.
LaTeX
$$$\\text{toOrderRingHom} : F \\to (\\alpha \\to+*o \\beta)$$$
Lean4
/-- Turn an element of a type `F` satisfying `OrderHomClass F α β` and `RingHomClass F α β`
into an actual `OrderRingHom`.
This is declared as the default coercion from `F` to `α →+*o β`. -/
@[coe]
def toOrderRingHom [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] [OrderHomClass F α β]
[RingHomClass F α β] (f : F) : α →+*o β :=
{ (f : α →+* β) with monotone' := OrderHomClass.monotone f }
