cyclic): |G|=expG ↔ G is cyclic (#10692)

Commit

4 years ago

feat(group_theory/specific_groups/cyclic): |G|=expG ↔ G is cyclic (#10692) Co-authored-by: Eric <37984851+ericrbg@users.noreply.github.com> Co-authored-by: Johan Commelin <johan@commelin.net>

Author

ericrbg

Parents

6c6c7da8

mathlib3 084b1ac2 - feat(group_theory/specific_groups/cyclic): |G|=expG ↔ G is cyclic (#10692)

mathlib3
084b1ac2 - feat(group_theory/specific_groups/cyclic): |G|=expG ↔ G is cyclic (#10692)