Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-11 23:56 50d3d5f4

View on Github →

feat(group_theory/index): Add typeclass for finite_index (#17139) Supersedes #14680.

Estimated changes

Modified src/group_theory/group_action/quotient.lean

Modified src/group_theory/index.lean

added theorem subgroup.finite_index_of_finite_quotient

added theorem subgroup.finite_index_of_le

Modified src/group_theory/p_group.lean

modified theorem is_p_group.index

Modified src/group_theory/schreier.lean

modified theorem subgroup.exists_finset_card_le_mul

deleted theorem subgroup.fg_of_index_ne_zero

modified theorem subgroup.rank_le_index_mul_rank

Modified src/group_theory/schur_zassenhaus.lean

Modified src/group_theory/sylow.lean

Modified src/group_theory/transfer.lean

modified theorem monoid_hom.transfer_center_eq_pow

deleted theorem monoid_hom.transfer_center_pow'_apply

modified theorem monoid_hom.transfer_center_pow_apply

modified theorem monoid_hom.transfer_def

modified theorem monoid_hom.transfer_eq_pow

modified theorem monoid_hom.transfer_eq_prod_quotient_orbit_rel_zpowers_quot