conj_inv

Mathlib.Algebra.Group.Conj

URI: https://scilib.ai/kg/mathlib#conj_inv

English

For any a,b in a group, the inverse of b a b^{-1} equals b a^{-1} b^{-1}.

Русский

Для любых a,b в группе обратное к b a b^{-1} равно b a^{-1} b^{-1}.

LaTeX

$$$ (b a b^{-1})^{-1} = b a^{-1} b^{-1} $$$

Lean4

theorem conj_inv {a b : α} : (b * a * b⁻¹)⁻¹ = b * a⁻¹ * b⁻¹ :=
  (map_inv (MulAut.conj b) a).symm

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

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

Разделы

Аффилиация

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