LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-08-03 (gpt-5.6-sol-codex-subscription)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The left cosets of a subgroup partition the group

Statement

For a subgroup $H \leq G$ , the set of distinct left cosets ${g H : g \in G}$ is a partition of $G$ : every element belongs to a left coset, every coset is nonempty, and two left cosets are either equal or disjoint.

Facts & Assumptions

Given: A group $G$ and a subgroup $H \leq G$ .

[F1]

A relation is an equivalence relation when it is reflexive, symmetric and transitive (Equivalence relation, equivalence class, and the quotient set $A / \sim$ ).

[L1]

The equivalence classes of an equivalence relation on a set are nonempty, cover the set and are pairwise equal or disjoint (The equivalence classes of an equivalence relation are nonempty, cover $A$ , and are pairwise equal or disjoint; conversely every such cover arises from exactly one equivalence relation).

[L2]

For $a, b \in G$ , $b \in a H$ if and only if $a^{- 1} b \in H$ , and $a H = b H$ if and only if $a^{- 1} b \in H$ ( $x \in a H$ iff $a^{- 1} x \in H$ , and $a H = b H$ iff $a^{- 1} b \in H$ ).

[F2]

Because $H \leq G$ , it contains the identity and is closed under inverses and products (Subgroup).

Proof

technique · direct

1.1givenF1F2L2

Define $a \sim b$ when $a^{- 1} b \in H$ . Since the given $H$ is a subgroup, $a^{- 1} a = e \in H$ , so the relation is reflexive.

1.2givenF1F2L2

If $a \sim b$ , then $a^{- 1} b \in H$ , so its inverse $b^{- 1} a$ belongs to $H$ and $b \sim a$ ; thus the relation is symmetric.

1.3givenF1F2L2

If $a \sim b$ and $b \sim c$ , subgroup closure gives $a^{- 1} c = (a^{- 1} b) (b^{- 1} c) \in H$ , so $a \sim c$ ; thus the relation is transitive.

2.1step 1.1step 1.2step 1.3F1L2

By steps 1.1 to 1.3, $\sim$ is an equivalence relation. Its class at $a$ is ${b : a^{- 1} b \in H} = a H$ by [L2].

The left cosets of a subgroup partition the group

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources