Mathlib v3 is deprecated. Go to Mathlib v4

Theorem subgroup.relindex_inf_mul_relindex

Modification history

2021-12-22 23:07
src/group_theory/index.lean
feat(group_theory/index): Transitivity of finite relative index. (#10936) …
Added subgroup.relindex_inf_mul_relindexView on Github →