self_trans_symm

Mathlib.Algebra.Order.Hom.Ring

URI: https://scilib.ai/kg/mathlib#OrderRingIso.self_trans_symm

English

Same as the previous self-transitivity with symmetry: (e.trans e.symm) = refl.

Русский

Как и ранее, повторно: (e.trans e.symm) = refl.

LaTeX

$$$\forall e:\alpha \overset{\text{OrderRingIso}}{\cong} \beta,\; e.trans e.symm = OrderRingIso.refl \alpha$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru