Commit 2024-07-18 16:07 84542b3e

View on Github →

refactor(GroupTheory/Complement,SchurZassenhaus): Replace Fintype.card with Nat.card (#14856) We're in the home stretch! This PR switches over GroupTheory/Complement and GroupTheory/SchurZassenhaus from Fintype.card to Nat.card.

Estimated changes

Modified Mathlib/GroupTheory/Complement.lean

modified theorem Subgroup.IsComplement'.card_mul

modified theorem Subgroup.IsComplement.card_mul

modified theorem Subgroup.isComplement'_iff_card_mul_and_disjoint

modified theorem Subgroup.isComplement'_of_card_mul_and_disjoint

modified theorem Subgroup.isComplement'_of_coprime

Modified Mathlib/GroupTheory/Nilpotent.lean

Modified Mathlib/GroupTheory/OrderOfElement.lean

modified theorem inf_eq_bot_of_coprime

Modified Mathlib/GroupTheory/SchurZassenhaus.lean

deleted theorem Subgroup.exists_left_complement'_of_coprime_of_fintype

deleted theorem Subgroup.exists_right_complement'_of_coprime_of_fintype