Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-18 12:36 cfa7f6af

View on Github →

feat(group_theory/index): Intersection of finite index subgroups (#12776) This PR proves that if H and K are of finite index in L, then so is H ⊓ K.

Estimated changes