conjNormal_symm_apply

Mathlib.GroupTheory.GroupAction.ConjAct

URI: https://scilib.ai/kg/mathlib#MulAut.conjNormal_symm_apply

← MathLib Explorer

English

The inverse inner automorphism acts by h ↦ g^{-1} h g.

Русский

Обратное внутреннее автоморфизм действует как h ↦ g^{-1} h g.

LaTeX

$$$ (MulAut.conjNormal(g))^{-1}(h) = g^{-1} h g. $$$

Lean4

@[simp]
theorem _root_.MulAut.conjNormal_symm_apply {H : Subgroup G} [H.Normal] (g : G) (h : H) :
    ↑((MulAut.conjNormal g).symm h) = g⁻¹ * h * g :=
  by
  change _ * _⁻¹⁻¹ = _
  rw [inv_inv]
  rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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