toOrderAddMonoidHom — Mathlib

English

If f and g are order ring homomorphisms α → β and f(a) = g(a) for all a ∈ α, then f = g; i.e., order-ring-homomorphisms are determined by their values pointwise.

Русский

Если f и g — порядковые кольцевые гомоморфизмы α → β и f(a) = g(a) для всех a ∈ α, то f = g; следовательно, их значения определяют морфизм по точкам.

LaTeX

$$$\\forall f,g : α \\to+*o β, (\\forall a, f(a) = g(a)) \\Rightarrow f = g$$$

Lean4

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

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