Commit 2023-06-06 04:38 aee19255

View on Github →

feat: port GroupTheory.Schreier (#4706)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/Schreier.lean

added def Subgroup.cardCommutatorBound

added theorem Subgroup.card_commutator_dvd_index_center_pow

added theorem Subgroup.card_commutator_le_of_finite_commutatorSet

added theorem Subgroup.closure_mul_image_eq

added theorem Subgroup.closure_mul_image_eq_top'

added theorem Subgroup.closure_mul_image_eq_top

added theorem Subgroup.closure_mul_image_mul_eq_top

added theorem Subgroup.exists_finset_card_le_mul

added theorem Subgroup.rank_le_index_mul_rank