Quotient_Group_of_Abelian_Group_is_Abelian
Provedabelian-groupsproofwikiquotient-groups
Let G be an abelian group and N a normal subgroup of G. Then the quotient group G/N is abelian.
Preamble
import Mathlib.GroupTheory.QuotientGroup.Basic
Formal statement
theorem Quotient_Group_of_Abelian_Group_is_Abelian {G : Type _} [CommGroup G] (N : Subgroup G) : ∀ a b : G ⧸ N, a * b = b * a := by sorrySource