Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-02 08:51 1b771af7

View on Github →

feat(group_theory/coset): card_dvd_of_injective (#8485)

Estimated changes

Modified src/group_theory/coset.lean

added theorem subgroup.card_comap_dvd_of_injective

added theorem subgroup.card_dvd_of_injective

added theorem subgroup.card_dvd_of_le