symm_trans_self — Mathlib

English

If e is an ordered ring isomorphism between two ordered rings α and β, then e has a two-sided inverse and composing it with e gives the identity on β.

Русский

Если e является упорядоченным кольцевым изоморфизмом между упорядоченными кольцами α и β, то у него есть двусторонний обратный, и композиция с e дает тождество на β.

LaTeX

$$$ e^{-1} \circ e = \mathrm{id}_{\beta} $$$

Lean4

@[simp]
theorem symm_trans_self (e : α ≃+*o β) : e.symm.trans e = OrderRingIso.refl β :=
  ext e.right_inv

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