Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-25 20:31 54212007

View on Github →

feat(group_theory/index): Small values of subgroup.index (#9893) H.index = 1 ↔ H = ⊤ and related results.

Estimated changes

added theorem subgroup.index_eq_one