Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-08 06:17 4dc96e4a

View on Github →

feat(group_theory/index): define the index of a subgroup (#8971) Defines subgroup.index and proves various divisibility properties.

Estimated changes

Modified src/group_theory/coset.lean

modified theorem subgroup.card_eq_card_quotient_mul_card_subgroup

added def subgroup.quotient_equiv_prod_of_le'

Created src/group_theory/index.lean

added theorem subgroup.index_dvd_card

added theorem subgroup.index_dvd_of_le

added theorem subgroup.index_eq_card

added theorem subgroup.index_eq_mul_of_le

added theorem subgroup.index_mul_card

Modified src/group_theory/quotient_group.lean

added def quotient_group.quotient_bot