mathlib
893f4800 - feat(group_theory/index): Lemmas for when `relindex` divides `index` (#14314)

Commit

3 years ago

feat(group_theory/index): Lemmas for when `relindex` divides `index` (#14314) This PR adds two lemmas for when `relindex` divides `index`.

Author

tb65536

Parents