self_trans_symm — Mathlib

English

For a ring equivalence e, the product e.trans e.symm is the identity on the source ring: e.trans e.symm = refl_R.

Русский

Для кольцевого эквивалента e произведение e.trans e.symm равно тождественному отображению на исходном кольце: e.trans e.symm = refl_R.

LaTeX

$$$ e.trans e.symm = RingEquiv.refl R $$$

Lean4

@[simp]
theorem self_trans_symm (e : R ≃+* S) : e.trans e.symm = RingEquiv.refl R :=
  ext e.left_inv

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