Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-17 11:06 a6158f19

View on Github →

feat(group_theory/subgroup/basic): One-sided closure induction lemmas (#12725) This PR adds one-sided closure induction lemmas, which I will need for Schreier's lemma.

Estimated changes