English
Given an order-monoid homomorphism f : M →*o N, there is a corresponding order homomorphism between archimedean classes: MulArchimedeanClass M →o MulArchimedeanClass N.
Русский
Для отображения с сохранением порядка f: M →*o N существует соответствующее отображение между архимедеанскими классами: MulArchimedeanClass M →o MulArchimedeanClass N.
LaTeX
$$$\\text{orderHom } f : \\MulArchimedeanClass M \\to\\to \\MulArchimedeanClass N$$$
Lean4
/-- An `OrderMonoidHom` can be lifted to an `OrderHom` over archimedean classes. -/
@[to_additive /-- An `OrderAddMonoidHom` can be lifted to an `OrderHom` over archimedean classes. -/
]
noncomputable def orderHom (f : M →*o N) : MulArchimedeanClass M →o MulArchimedeanClass N :=
(MulArchimedeanOrder.orderHom f).antisymmetrization
