Commit 2024-06-06 06:18 e3892bc4

View on Github →

Refactor(Algebra/Group/Subgroup/Finite): Replace Fintype.card with Nat.card (#13432) A lot of the group theory library still needs to be switched over from Fintype.card to Nat.card. This PR switches over Algebra/Group/Subgroup/Finite.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/Algebra/Group/Subgroup/Finite.lean

modified theorem Subgroup.card_bot

modified theorem Subgroup.card_eq_iff_eq_top

modified theorem Subgroup.card_le_card_group

modified theorem Subgroup.card_le_one_iff_eq_bot

modified theorem Subgroup.card_top

modified theorem Subgroup.eq_bot_iff_card

modified theorem Subgroup.eq_bot_of_card_eq

modified theorem Subgroup.eq_bot_of_card_le

modified theorem Subgroup.eq_top_of_card_eq

modified theorem Subgroup.eq_top_of_le_card

modified theorem Subgroup.one_lt_card_iff_ne_bot

Modified Mathlib/GroupTheory/Nilpotent.lean

Modified Mathlib/GroupTheory/PGroup.lean

Modified Mathlib/GroupTheory/SchurZassenhaus.lean

Modified Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

added theorem Subgroup.eq_bot_or_eq_top_of_prime_card

Modified Mathlib/GroupTheory/Sylow.lean