Mathlib v3 is deprecated. Go to Mathlib v4

Theorem subgroup.relindex_eq_one

Modification history

2022-11-17 22:56

src/group_theory/index.lean

feat(group_theory/index): Add `iff`-lemmas `relindex_eq_one` and `card_eq_one` (#17271) …

Added subgroup.relindex_eq_one View on Github →