Commit 2024-08-11 23:33 e848aeef

View on Github →

refactor(Cyclic): redefine, move definition (#15544) Redefine IsCyclic without Subgroup dependency, move the definition to Algebra/Group/Defs.

Estimated changes

Modified Mathlib/Algebra/Group/Defs.lean

added theorem exists_zpow_surjective

Modified Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

added theorem IsCyclic.exists_generator

Modified Mathlib/Logic/Function/Defs.lean