basic): Cyclic subgroups are commutative (#13663)

Commit

3 years ago

feat(group_theory/subgroup/basic): Cyclic subgroups are commutative (#13663) This PR adds an instance stating that the cyclic subgroups `zpowers g` are commutative.

Author

tb65536

Parents

b0fe3cd2

mathlib ef3769db - feat(group_theory/subgroup/basic): Cyclic subgroups are commutative (#13663)

mathlib
ef3769db - feat(group_theory/subgroup/basic): Cyclic subgroups are commutative (#13663)