trans_toRingEquiv — Mathlib

English

The underlying ring equivalence of the trans of two order ring isos equals the trans of their underlying ring equivalences.

Русский

Уподобляющееся кольцевое эквивалентное преобразование двух OrderRingIso сохраняется через транспозицию их базовых RingEquiv.

LaTeX

$$$ (OrderRingIso.trans f g).toRingEquiv = RingEquiv.trans f.toRingEquiv g.toRingEquiv $$$

Lean4

/-- This lemma used to be generated by [simps] on `trans`, but the lhs of this simplifies under
simp. Removed [simps] attribute and added aux version below. -/
theorem trans_toRingEquiv (f : α ≃+*o β) (g : β ≃+*o γ) :
    (OrderRingIso.trans f g).toRingEquiv = RingEquiv.trans f.toRingEquiv g.toRingEquiv :=
  rfl

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