of_conjugate_fixed — Mathlib

English

If conjugation by every g fixes H, then H is a normal subgroup.

Русский

Если сопряжение каждое g фиксирует H, то H является нормальной подгруппой.

LaTeX

$$$ (\forall g : G, (\mathrm{MulAut.conj}(g) \cdot H) = H) \Rightarrow H \trianglelefteq G $$$

Lean4

theorem of_conjugate_fixed {H : Subgroup G} (h : ∀ g : G, (MulAut.conj g) • H = H) : H.Normal :=
  by
  constructor
  intro n hn g
  rw [← h g, Subgroup.mem_pointwise_smul_iff_inv_smul_mem, ← map_inv, MulAut.smul_def, MulAut.conj_apply, inv_inv,
    mul_assoc, mul_assoc, inv_mul_cancel, mul_one, ← mul_assoc, inv_mul_cancel, one_mul]
  exact hn

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