Commit 2021-10-19 23:43 2d17c5a2

View on Github →

feat(group_theory/index): Relative index (#9780) Defines relative index between subgroups, and proves that relative index is multiplicative in towers.

Estimated changes

Modified src/group_theory/index.lean

added theorem subgroup.index_comap

deleted theorem subgroup.index_eq_mul_of_le

added theorem subgroup.relindex_mul_index

added theorem subgroup.relindex_mul_relindex

added theorem subgroup.relindex_subgroup_of