English
Let G be a group and H ≤ G. The index [G : H] is equal to 2 if and only if there exists an element a ∈ G such that for every b ∈ G exactly one of ba ∈ H or b ∈ H holds.
Русский
Пусть G — группа и H ≤ G. Индекс [G : H] равен 2 тогда и только тогда, когда существует элемент a ∈ G такой, что для каждого b ∈ G ровно одно из условий ba ∈ H и b ∈ H верно.
LaTeX
$$$ [G: H] = 2 \iff \exists a \in G, \ \forall b \in G,\ (ba \in H) \oplus (b \in H). $$$
Lean4
/-- A subgroup has index two if and only if there exists `a` such that for all `b`, exactly one
of `b * a` and `b` belong to `H`. -/
@[to_additive /-- An additive subgroup has index two if and only if there exists `a` such that
for all `b`, exactly one of `b + a` and `b` belong to `H`. -/
]
theorem index_eq_two_iff : H.index = 2 ↔ ∃ a, ∀ b, Xor' (b * a ∈ H) (b ∈ H) :=
by
simp only [index, Nat.card_eq_two_iff' ((1 : G) : G ⧸ H), ExistsUnique, inv_mem_iff, QuotientGroup.exists_mk,
QuotientGroup.forall_mk, Ne, QuotientGroup.eq, mul_one, xor_iff_iff_not]
refine exists_congr fun a => ⟨fun ha b => ⟨fun hba hb => ?_, fun hb => ?_⟩, fun ha => ⟨?_, fun b hb => ?_⟩⟩
· exact ha.1 ((mul_mem_cancel_left hb).1 hba)
· exact inv_inv b ▸ ha.2 _ (mt (inv_mem_iff (x := b)).1 hb)
· rw [← inv_mem_iff (x := a), ← ha, inv_mul_cancel]
exact one_mem _
· rwa [ha, inv_mem_iff (x := b)]
