Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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≤GH\le G, the set of distinct left cosets {gH:g∈G}\{gH:g\in G\} is a partition of GG: 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 GG and a subgroup H≤GH\le G.

[F1]

A relation is an equivalence relation when it is reflexive, symmetric and transitive (Equivalence relation, equivalence class, and the quotient set A/∼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 AA, and are pairwise equal or disjoint; conversely every such cover arises from exactly one equivalence relation).

[L2]

For a,b∈Ga,b\in G, b∈aHb\in aH if and only if a−1b∈Ha^{-1}b\in H, and aH=bHaH=bH if and only if a−1b∈Ha^{-1}b\in H (x∈aHx\in aH iff a−1x∈Ha^{-1}x\in H, and aH=bHaH=bH iff a−1b∈Ha^{-1}b\in H).

[F2]

Because H≤GH\le G, it contains the identity and is closed under inverses and products (Subgroup).

Proof

technique · direct
1.1

Define a∼ba\sim b when a−1b∈Ha^{-1}b\in H. Since the given HH is a subgroup, a−1a=e∈Ha^{-1}a=e\in H, so the relation is reflexive.

givenF1F2L2
1.2

If a∼ba\sim b, then a−1b∈Ha^{-1}b\in H, so its inverse b−1ab^{-1}a belongs to HH and b∼ab\sim a; thus the relation is symmetric.

givenF1F2L2
1.3

If a∼ba\sim b and b∼cb\sim c, subgroup closure gives a−1c=(a−1b)(b−1c)∈Ha^{-1}c=(a^{-1}b)(b^{-1}c)\in H, so a∼ca\sim c; thus the relation is transitive.

givenF1F2L2
2.1

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

step 1.1step 1.2step 1.3F1L2
3.1

The conclusion follows from [L1] applied to these equivalence classes.

step 2.1L1∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 36 results over 18 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources