inducedOrderRingIso_self — Mathlib

English

The induced order ring isomorphism on β with itself is the identity isomorphism.

Русский

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

LaTeX

$$$ \mathrm{inducedOrderRingIso} \beta \beta = \mathrm{OrderRingIso.refl} \beta $$$

Lean4

@[simp]
theorem inducedOrderRingIso_self : inducedOrderRingIso β β = OrderRingIso.refl β :=
  OrderRingIso.ext inducedMap_self

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