Commit 2022-10-24 07:29 3882aaf6

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

• 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).