symm_comp_self

Mathlib.Algebra.Order.Hom.Monoid

URI: https://scilib.ai/kg/mathlib#OrderMonoidIso.symm_comp_self

English

The left inverse behavior: e.symm ∘ e = id.

Русский

Лёвый инверсный поведение: e.symm ∘ e = id.

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem symm_comp_self (e : α ≃*o β) : e.symm ∘ e = id :=
  funext e.symm_apply_apply

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

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

Разделы

Аффилиация

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