Commit 2022-11-17 22:56 c00ed312

View on Github →

feat(group_theory/index): Add iff-lemmas relindex_eq_one and card_eq_one (#17271) This PR adds iff-lemmas relindex_eq_one and card_eq_one.

Estimated changes

Modified src/group_theory/index.lean

added theorem subgroup.card_eq_one

added theorem subgroup.relindex_eq_one

Modified src/group_theory/subgroup/basic.lean

added theorem subgroup.subgroup_of_eq_bot

added theorem subgroup.subgroup_of_eq_top