mathlib3

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

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