comp_symm

Mathlib.RingTheory.Bialgebra.Equiv

URI: https://scilib.ai/kg/mathlib#BialgEquiv.comp_symm

English

The composition of a bialgebra equivalence with its inverse is the identity on B.

Русский

Композиция биалгебрового эквивалентности с его обратной равна единице на B.

LaTeX

$$$(e) \\circ (e^{\\mathrm{symm}}) = \\mathrm{id}_{B}$$$

Lean4

@[simp]
theorem comp_symm (e : A ≃ₐc[R] B) : (e : A →ₐc[R] B).comp e.symm = .id R B :=
  BialgHom.coe_algHom_injective e.toAlgEquiv.comp_symm

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

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

Разделы

Аффилиация

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