coe_toOrderRingHom_refl — Mathlib

English

The identity order-ring isomorphism corresponds to the identity order-ring hom.

Русский

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

LaTeX

$$$ (\operatorname{OrderRingIso.refl} \alpha : \alpha \to+*o \alpha) = \operatorname{OrderRingHom.id} \alpha $$$

Lean4

@[simp]
theorem coe_toOrderRingHom_refl : (OrderRingIso.refl α : α →+*o α) = OrderRingHom.id α :=
  rfl

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