toOrderMonoidWithZeroHom — Mathlib

English

For any e, the relation e.symm x = y is equivalent to x = e y.

Русский

Для любого e отношение e.symm x = y эквивалентно x = e y.

LaTeX

$$$e^{-1} x = y \\iff x = e y$$$

Lean4

/-- Turn an element of a type `F`
satisfying `OrderHomClass F α β` and `MonoidWithZeroHomClass F α β`
into an actual `OrderMonoidWithZeroHom`.
This is declared as the default coercion from `F` to `α →+*₀o β`. -/
@[coe]
def toOrderMonoidWithZeroHom [OrderHomClass F α β] [MonoidWithZeroHomClass F α β] (f : F) : α →*₀o β :=
  { (f : α →*₀ β) with monotone' := OrderHomClass.monotone f }

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