Abelian_Quotient_Group_v2
Provedabeliancommutatorgroup-theoryproofwikiquotient-group
The quotient group G/N is abelian if and only if N contains every commutator aba⁻¹b⁻¹.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Abelian_Quotient_Group_v2 {G : Type _} [Group G] (N : Subgroup G) [N.Normal] : (∀ (a b : G), (QuotientGroup.mk' N) (a * b) = (QuotientGroup.mk' N) (b * a)) ↔ (∀ (a b : G), a * b * a⁻¹ * b⁻¹ ∈ N) := by sorrySource