normalCore_eq_iInf_conjAct — Mathlib

English

The normal core of H equals the infimum of all conjugates of H under ConjAct G: H.normalCore = ⨅ (g : ConjAct G), g • H.

Русский

Ядро нормальности H равно инфимума всех сопряжённых H по действию ConjAct G: H.normalCore = ⨅ (g : ConjAct G), g • H.

LaTeX

$$$ H.normalCore = \bigwedge_{g : ConjAct(G)} g \cdot H $$$

Lean4

theorem normalCore_eq_iInf_conjAct (H : Subgroup G) : H.normalCore = ⨅ (g : ConjAct G), g • H :=
  by
  ext g
  simp only [Subgroup.normalCore, Subgroup.mem_iInf, Subgroup.mem_pointwise_smul_iff_inv_smul_mem]
  refine ⟨fun h x ↦ h x⁻¹, fun h x ↦ ?_⟩
  simpa only [ConjAct.toConjAct_inv, inv_inv] using h x⁻¹

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