normal_of_eq_cosets — Mathlib

English

If for all g, the left coset g s equals the right coset by g, then s is a normal subgroup.

Русский

Если для всех g левая косета g s равна правой косете g s, тогда s нормальна.

LaTeX

$$$\forall g,\; g s = s g \Rightarrow s \text{ is normal}$$$

Lean4

@[to_additive normal_of_eq_addCosets]
theorem normal_of_eq_cosets (h : ∀ g : α, g • (s : Set α) = op g • s) : s.Normal :=
  ⟨fun a ha g => show g * a * g⁻¹ ∈ (s : Set α) by rw [← mem_rightCoset_iff, ← h]; exact mem_leftCoset g ha⟩

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