feat(group_theory/index): criterion for subgroups of index two

[urkud]

• A subgroup has index two if and only if there exists a such that for all b, b * a ∈ H is equivalent to b ∉ H.
• For a subgroup of index two, a * b ∈ H ↔ (a ∈ H ↔ b ∈ H).

---

• [x] depends on: #16898
• [x] depends on: #16899

[jcommelin]

This currently contains your review of "cubing the cube". Did some rebase go wrong?

[urkud]

This currently contains your review of "cubing the cube". Did some rebase go wrong?

No, I touched API about 2 ≤ cardinal.mk α, this broke cubing_a_cube, so I migrated the latter to nontrivial. Then I forgot to list dependencies in this PR.

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib#16898~~
• ~~leanprover-community/mathlib#16899~~ By Dependent Issues (🤖). Happy coding!

[urkud]

@jcommelin Merged master.

[bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests