coe_orderAddMonoidHom_id — Mathlib

English

The underlying order-add-monoid hom of the identity order ring hom equals the identity order-add-monoid hom.

Русский

У подлежащего гомоморфизма-упорядоченного моноида Id он равен идентичности для OrderAddMonoid.

LaTeX

$$$\operatorname{coe}(OrderRingHom.id\alpha) = OrderAddMonoidHom.id\alpha$$$

Lean4

@[simp]
theorem coe_orderAddMonoidHom_id : (OrderRingHom.id α : α →+o α) = OrderAddMonoidHom.id α :=
  rfl

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