Commit 2024-11-18 09:35 66df24a8

View on Github →

refactor(GroupTheory/SpecificGroups/Cyclic): Switch from Fintype to Finite (#19109) This PR switches most of GroupTheory/SpecificGroups/Cyclic.lean from Fintype to Finite.

Estimated changes

Modified Mathlib/FieldTheory/Finite/Basic.lean

Modified Mathlib/GroupTheory/Exponent.lean

Modified Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

modified theorem CommGroup.is_simple_iff_isCyclic_and_prime_card

modified theorem IsCyclic.exponent_eq_card

modified theorem IsCyclic.ext

modified theorem IsCyclic.iff_exponent_eq_card

modified theorem IsCyclic.of_exponent_eq_card

modified theorem IsSimpleGroup.prime_card

modified theorem Subgroup.eq_bot_or_eq_top_of_prime_card

modified theorem exists_pow_ne_one_of_isCyclic

modified theorem isCyclic_of_orderOf_eq_card

modified theorem isCyclic_of_prime_card

modified theorem isSimpleGroup_of_prime_card

modified theorem mem_powers_of_prime_card

modified theorem mem_zpowers_of_prime_card

modified theorem orderOf_eq_card_of_forall_mem_zpowers

deleted theorem orderOf_generator_eq_natCard

modified theorem powers_eq_top_of_prime_card

modified theorem zpowers_eq_top_of_prime_card

Modified Mathlib/GroupTheory/SpecificGroups/Quaternion.lean

Modified Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean

Modified Mathlib/NumberTheory/LucasPrimality.lean

Modified Mathlib/NumberTheory/MulChar/Lemmas.lean

Modified Mathlib/RingTheory/RootsOfUnity/Basic.lean

modified def IsCyclic.monoidHomMulEquivRootsOfUnityOfGenerator

modified theorem IsCyclic.monoidHom_mulEquiv_rootsOfUnity

Modified Mathlib/RingTheory/RootsOfUnity/EnoughRootsOfUnity.lean