toOrderRingHom_eq_coe — Mathlib

English

Viewing an order ring isomorphism as an order ring hom, its action on elements agrees with the original map.

Русский

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

LaTeX

$$$ f.toOrderRingHom = f $$$

Lean4

@[simp]
theorem toOrderRingHom_eq_coe (f : α ≃+*o β) : f.toOrderRingHom = f :=
  rfl

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