eq_cosets_of_normal — Mathlib

English

Let N be normal in G. Then for all g ∈ G, the left coset g N equals the right coset N g.

Русский

Пусть N нормальна в G. Тогда для всякого g ∈ G левый косет g N равен правому косету N g.

LaTeX

$$$N \trianglelefteq G \implies \forall g \in G,\; g N = N g$$$

Lean4

@[to_additive eq_addCosets_of_normal]
theorem eq_cosets_of_normal (N : s.Normal) (g : α) : g • (s : Set α) = op g • s :=
  Set.ext fun a => by simp [mem_leftCoset_iff, mem_rightCoset_iff, N.mem_comm_iff]

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