toOrderRingHom_injective — Mathlib

English

The map from order-ring-isomorphisms to order-ring-homs is injective.

Русский

Обратная карта из упорядоченных кольцевых изоморфизмов в упорядоченные кольцевые гомоморфизмы инъективна.

LaTeX

$$$ \operatorname{Injective}(\operatorname{toOrderRingHom}) $$$

Lean4

theorem toOrderRingHom_injective : Injective (toOrderRingHom : α ≃+*o β → α →+*o β) := fun f g h =>
  DFunLike.coe_injective <| by convert DFunLike.ext'_iff.1 h using 0

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