Commit 2024-07-17 06:20 26f108b3

View on Github →

refactor(GroupTheory/PGroup,Sylow): Replace Fintype.card with Nat.card (#14789) A lot of the group theory library still needs to be switched over from Fintype.card to Nat.card. This PR switches over GroupTheory/PGroup.lean and GroupTheory/Sylow (there was enough dependence between the two that it was simplest to do them together).

Estimated changes

Modified Mathlib/GroupTheory/Nilpotent.lean

Modified Mathlib/GroupTheory/PGroup.lean

modified theorem IsPGroup.card_center_eq_prime_pow

modified theorem IsPGroup.card_modEq_card_fixedPoints

modified theorem IsPGroup.card_orbit

modified def IsPGroup.commGroupOfCardEqPrimeSq

modified theorem IsPGroup.commutative_of_card_eq_prime_sq

modified theorem IsPGroup.cyclic_center_quotient_of_card_eq_prime_sq

modified theorem IsPGroup.exists_fixed_point_of_prime_dvd_card_of_fixed_point

modified theorem IsPGroup.iff_card

modified theorem IsPGroup.nonempty_fixed_point_of_prime_not_dvd_card

modified theorem IsPGroup.nontrivial_iff_card

modified theorem IsPGroup.of_card

Modified Mathlib/GroupTheory/Perm/Cycle/Type.lean

added theorem exists_prime_orderOf_dvd_card'

Modified Mathlib/GroupTheory/SchurZassenhaus.lean

Modified Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

added theorem isCyclic_of_card_dvd_prime

Modified Mathlib/GroupTheory/Sylow.lean

modified theorem QuotientGroup.card_preimage_mk

modified theorem Sylow.card_coprime_index

modified theorem Sylow.card_eq_multiplicity

modified theorem Sylow.card_normalizer_modEq_card

modified theorem Sylow.card_quotient_normalizer_modEq_card_quotient

modified theorem Sylow.coe_ofCard

modified theorem Sylow.dvd_card_of_dvd_card

modified theorem Sylow.exists_subgroup_card_pow_prime

modified theorem Sylow.exists_subgroup_card_pow_prime_le

modified theorem Sylow.exists_subgroup_card_pow_succ

added theorem Sylow.finite_of_injective

added theorem Sylow.finite_of_ker_is_pGroup

modified theorem Sylow.ne_bot_of_dvd_card

modified def Sylow.ofCard

modified theorem Sylow.pow_dvd_card_of_pow_dvd_card

modified theorem Sylow.prime_dvd_card_quotient_normalizer

modified theorem Sylow.prime_pow_dvd_card_normalizer

modified theorem card_sylow_dvd_index

modified theorem card_sylow_eq_card_quotient_normalizer

modified theorem card_sylow_eq_index_normalizer

modified theorem card_sylow_modEq_one

modified theorem not_dvd_card_sylow