Commit 2024-06-08 03:30 480278c4

View on Github →

refactor(GroupTheory/Coset): Replace Fintype.card with Nat.card (#13431) A lot of the group theory library still needs to be switched over from Fintype.card to Nat.card. This PR switches over GroupTheory/Coset.lean. I had to add a little noise to a few other files, but these will get cleaned up once those files are switched over later.

Estimated changes

Modified Mathlib/GroupTheory/Coset.lean

modified theorem Subgroup.card_comap_dvd_of_injective

modified theorem Subgroup.card_dvd_of_injective

modified theorem Subgroup.card_dvd_of_le

modified theorem Subgroup.card_eq_card_quotient_mul_card_subgroup

modified theorem Subgroup.card_quotient_dvd_card

modified theorem Subgroup.card_subgroup_dvd_card

Modified Mathlib/GroupTheory/Nilpotent.lean

Modified Mathlib/GroupTheory/Order/Min.lean

Modified Mathlib/GroupTheory/PGroup.lean

Modified Mathlib/GroupTheory/SchurZassenhaus.lean

Modified Mathlib/GroupTheory/SpecificGroups/Alternating.lean

Modified Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

Modified Mathlib/GroupTheory/Sylow.lean

Modified Mathlib/NumberTheory/NumberField/Embeddings.lean