invFun_eq_symm

Mathlib.RingTheory.Bialgebra.Equiv

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

English

The inverse function e.invFun of a bialgebra equivalence e equals its symmetry map e.symm.

Русский

Обратная функция e.invFun эквивалентности e равна ее симметрической карте e.symm.

LaTeX

$$$e^{-1}_{\\mathrm{fun}} = e.zip$$$

Lean4

theorem invFun_eq_symm : e.invFun = e.symm :=
  rfl

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

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

Разделы

Аффилиация

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