mathlib3
cfa7f6af - feat(group_theory/index): Intersection of finite index subgroups (#12776)

Commit

3 years ago

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`.

Author

tb65536

Parents

5ecd27ad

mathlib3 cfa7f6af - feat(group_theory/index): Intersection of finite index subgroups (#12776)

mathlib3
cfa7f6af - feat(group_theory/index): Intersection of finite index subgroups (#12776)