Mathlib v3 is deprecated. Go to Mathlib v4

Theorem commutative_of_cyclic_center_quotient

Modification history

2021-06-22 11:36

src/group_theory/specific_groups/cyclic.lean

feat(group_theory/specific_groups/cyclic): A group is commutative if the quotient by the center is cyclic (#7952)

Added commutative_of_cyclic_center_quotient View on Github →