Commit 2023-11-28 08:56 666326ce

View on Github →

feat: add some results about IsCyclic (#8625) From flt-regular.

Estimated changes

Modified Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

added theorem isAddCyclic_additive_iff

added theorem isCyclic_multiplicative_iff

added theorem isCyclic_of_surjective