Commit 2021-10-21 11:25 777f11c8

View on Github →

feat(group_theory/index): Special cases of relindex (#9831) Adds special cases of relindex. Also refactors the file to use nat.card, rather than the equivalent (# _).to_nat.

Estimated changes

Modified src/group_theory/index.lean

modified theorem subgroup.index_bot

added theorem subgroup.relindex_bot_left

added theorem subgroup.relindex_bot_left_eq_card

added theorem subgroup.relindex_bot_right

added theorem subgroup.relindex_self

added theorem subgroup.relindex_top_left

added theorem subgroup.relindex_top_right