Commit 2024-11-15 10:35 c6da505b

View on Github →

refactor(GroupTheory/SpecificGroups/Cyclic): Use variables (#19075) This PR refactors GroupTheory/SpecificGroups/Cyclic.lean to use variables.

Estimated changes

Modified Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

modified theorem IsCyclic.ext

modified theorem MonoidHom.map_cyclic

modified theorem Subgroup.eq_bot_or_eq_top_of_prime_card

modified theorem Subgroup.isCyclic_of_le

modified def commGroupOfCyclicCenterQuotient

modified theorem commutative_of_cyclic_center_quotient

modified theorem exists_pow_ne_one_of_isCyclic

modified theorem isCyclic_of_card_dvd_prime

modified theorem isCyclic_of_prime_card

modified theorem isCyclic_of_surjective

modified theorem isSimpleGroup_of_prime_card

modified theorem mem_powers_of_prime_card

modified theorem mem_zpowers_of_prime_card

modified theorem powers_eq_top_of_prime_card

modified theorem zpowers_eq_top_of_prime_card