comp — Mathlib

English

The composition of two order ring homomorphisms is again an order ring homomorphism.

Русский

Композитность двух упорядоченных кольцевых гомоморфизмов даёт снова упорядоченный кольцевой гомоморфизм.

LaTeX

$$$f\circ g \text{ is an order ring homomorphism }\alpha \to+*o \gamma$$$

Lean4

/-- Composition of two `OrderRingHom`s as an `OrderRingHom`. -/
protected def comp (f : β →+*o γ) (g : α →+*o β) : α →+*o γ :=
  { f.toRingHom.comp g.toRingHom, f.toOrderAddMonoidHom.comp g.toOrderAddMonoidHom with }

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