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

Commit

3 years ago

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`.

Author

tb65536

Parents

1330a700

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

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