commutator_closure_isNormal — Mathlib

English

The commutator closure of the absolute Galois group is a normal subgroup in its topological closure.

Русский

Замыкание коммутатора абсолютной Галуа-группы является нормальной подгруппой в её топологическом замыкании.

LaTeX

$$$$\big(\mathrm{commutator}(\mathrm{Field.absoluteGaloisGroup}\,K)\big)_{\text{topologicalClosure}}.Normal$$$$

Lean4

instance commutator_closure_isNormal : (commutator (G_K K)).topologicalClosure.Normal :=
  Subgroup.is_normal_topologicalClosure (commutator (G_K K))

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