Commit 2024-07-15 20:56 f53d6a19

View on Github →

refactor(GroupTheory/Index): Replace Fintype.card with Nat.card (#13630) A lot of the group theory library still needs to be switched over from Fintype.card to Nat.card. This PR switches over GroupTheory/Index.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. In this file there were a few Fintype.card lemmas whose Nat.card lemmas already existed, so I deleted those rather than switching them over (they are not just redundant, but strictly weaker since they assume finiteness).

Estimated changes

modified theorem Subgroup.dvd_index_map
modified theorem Subgroup.index_comap
modified theorem Subgroup.index_dvd_card
modified theorem Subgroup.index_eq_card
modified theorem Subgroup.index_ker
modified theorem Subgroup.index_map
modified theorem Subgroup.index_map_dvd
modified theorem Subgroup.index_map_eq
modified theorem Subgroup.index_mul_card
modified theorem Subgroup.relindex_comap
modified theorem Subgroup.relindex_ker