toOrderMonoidWithZeroHom — Mathlib

English

An ordered ring homomorphism f: α →+*o β can be reinterpreted as an order-additive-monoid-homomorphism α →+o β by forgetting the multiplicative structure while keeping the monotonicity.

Русский

Пусть f: α →+*o β — упорядоченный кольцевой гомоморфизм. Его можно переопределить как упорядоченный аддитивный моноидный гомоморфизм α →+o β, забывая про умножение, сохраняя монотонность.

LaTeX

$$$\\mathrm{toOrderAddMonoidHom} : (α \\to+*o β) \\to (α \\to+o β)$$$

Lean4

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

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