coe_toOrderRingHom — Mathlib

English

Coefficient-level coercion of an order ring iso to an order ring hom preserves the underlying function.

Русский

Приведение по коэффициентам из упорядоченного кольцевого изоморфизма к упорядоченному кольцевому гомоморфизму сохраняет базовую функцию.

LaTeX

$$$ \big( f : \alpha \simeq_o \beta \big) : \alpha \to+*o \beta = f $$$

Lean4

@[simp, norm_cast]
theorem coe_toOrderRingHom (f : α ≃+*o β) : ⇑(f : α →+*o β) = f :=
  rfl

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