Commit 2026-03-23 15:54 1b158561

View on Github →

chore(GroupTheory/SpecificGroups/Cyclic/Basic): refactor (#36983) Refactor GroupTheory/SpecificGroups/Cyclic.lean by putting a first batch of lemmas in GroupTheory/SpecificGroups/Cyclic/Basic, when they are compatible with assert_not_exists Field. The issue with the pre-PR situation is that the initial assumption assert_not_exists Field is incompatible with the use of tactics (interval_cases or gcongr) which use whatever they can.

Estimated changes

deleted def IsCyclic.commGroup
deleted theorem IsCyclic.exists_generator
deleted theorem IsCyclic.ext
deleted theorem IsCyclic.image_range_card
deleted theorem IsCyclic.unique_zpow_zmod
deleted theorem MonoidHom.map_cyclic
deleted theorem MulEquiv.isCyclic
deleted theorem Subgroup.isCyclic_of_le
deleted theorem Subgroup.le_zpowers_iff
deleted theorem isAddCyclic_additive_iff
deleted theorem isCyclic_of_injective
deleted theorem isCyclic_of_prime_card
deleted theorem isCyclic_of_surjective
deleted theorem mem_powers_of_prime_card
deleted theorem mem_zpowers_of_prime_card
added theorem IsCyclic.ext
added theorem MonoidHom.map_cyclic
added theorem MulEquiv.isCyclic
added theorem isCyclic_of_injective
added theorem isCyclic_of_prime_card
added theorem isCyclic_of_surjective