toOrderRingHom — Mathlib

English

Every ordered ring isomorphism f yields an ordered ring homomorphism f.toOrderRingHom.

Русский

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

LaTeX

$$$ \operatorname{toOrderRingHom}(f) : \alpha \to+*o \beta $$$

Lean4

/-- Reinterpret an ordered ring isomorphism as an ordered ring homomorphism. -/
def toOrderRingHom (f : α ≃+*o β) : α →+*o β :=
  ⟨f.toRingEquiv.toRingHom, fun _ _ => (map_le_map_iff f).2⟩

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