conj_symm

Mathlib.Logic.Equiv.Defs

URI: https://scilib.ai/kg/mathlib#Equiv.conj_symm

English

The conjugation by e and the conjugation by its inverse e^{-1} are inverse to each other: conj(e)^{-1} = conj(e^{-1}).

Русский

Сопряжение по e и сопряжение по обратному e^{-1} взаимно обращаются: conj(e)^{-1} = conj(e^{-1}).

LaTeX

$$$ \operatorname{conj}(e)^{-1} = \operatorname{conj}(e^{-1}). $$$

Lean4

@[simp, grind =]
theorem conj_symm (e : α ≃ β) : e.conj.symm = e.symm.conj :=
  rfl

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

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

Разделы

Аффилиация

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