Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-20 18:03 3d00081c

View on Github →

feat(group_theory/index): Index of top and bottom subgroups (#9819) This PR computes the index of the top and bottom subgroups.

Estimated changes

added theorem subgroup.index_bot
added theorem subgroup.index_top
modified theorem cardinal.one_to_nat
added theorem cardinal.to_nat_eq_one
modified theorem cardinal.zero_to_nat