mathlib3
a1b96f80 - feat(group_theory/index): Index of finite intersection (#16393)

Commit

3 years ago

feat(group_theory/index): Index of finite intersection (#16393) This PR proves that the index of a finite intersection is at most the product of the indices.

Author

tb65536

Parents

ec0b1144

mathlib3 a1b96f80 - feat(group_theory/index): Index of finite intersection (#16393)

mathlib3
a1b96f80 - feat(group_theory/index): Index of finite intersection (#16393)