normal_iff_eq_cosets — Mathlib

English

A subgroup s is normal in α if and only if for every g ∈ α, left coset g s equals right coset by g.

Русский

Подгруппа s нормальна тогда и только тогда, когда для каждого g ∈ α левая косета g s равна правой косете by g.

LaTeX

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

Lean4

@[to_additive normal_iff_eq_addCosets]
theorem normal_iff_eq_cosets : s.Normal ↔ ∀ g : α, g • (s : Set α) = op g • s :=
  ⟨@eq_cosets_of_normal _ _ s, normal_of_eq_cosets s⟩

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