Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Def
comm_group_of_cycle_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
comm_group_of_cycle_center_quotient
View on Github →