conj_smul_eq_self

Mathlib.Algebra.Group.Subgroup.Pointwise

URI: https://scilib.ai/kg/mathlib#Subgroup.Normal.conj_smul_eq_self

English

Conjugation action fixes H when H is normal, i.e., any ConjAct element preserves H.

Русский

Действие сопряжения фиксирует H, если H нормальная; любой элемент ConjAct сохраняет H.

LaTeX

$$$ g \cdot H = H $ for all $g \in \mathrm{ConjAct}(G)$$$

Lean4

@[simp]
theorem conj_smul_eq_self (g : G) (H : Subgroup G) [h : Normal H] : MulAut.conj g • H = H :=
  h.conjAct g

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

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

Разделы

Аффилиация

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