toOrderMonoidHom — Mathlib

English

An ordered monoid with zero homomorphism f can be interpreted as an ordinary order monoid homomorphism, with the underlying map agreeing with f.

Русский

Упорядоченный моноидовый гомоморфизм с нулём f можно рассматривать как обычный упорядоченный моноидогомоморфизм; базовая функция совпадает с f.

LaTeX

$$$\text{toOrderMonoidHom}(f) = f$ (as functions)$$

Lean4

/-- Reinterpret an ordered monoid with zero homomorphism as an order monoid homomorphism. -/
def toOrderMonoidHom (f : α →*₀o β) : α →*o β :=
  { f with }

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