English
A functorial transformation from an order-homomorphism class to an actual ordered monoid-with-zero homomorphism preserves structure.
Русский
Функциональное преобразование из класса порядок-хомоморфизмов в конкретный порядок-монойд с нулём сохраняет структуру.
LaTeX
$$$\\text{toOrderMonoidWithZeroHom}$$$
Lean4
/-- Makes an ordered group isomorphism from a proof that the map preserves multiplication. -/
@[to_additive /-- Makes an ordered additive group isomorphism from a proof that the map preserves
addition. -/
]
def mk' (f : α ≃ β) (hf : ∀ {a b}, f a ≤ f b ↔ a ≤ b) (map_mul : ∀ a b : α, f (a * b) = f a * f b) : α ≃*o β :=
{ MulEquiv.mk' f map_mul with map_le_map_iff' := hf }
