LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-01

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.

$x \in a H$ iff $a^{- 1} x \in H$ , and $a H = b H$ iff $a^{- 1} b \in H$

Statement

Let $H \leq G$ and let $a, b, x \in G$ . Then

$x \in a H ⟺ a^{- 1} x \in H,$

and

$a H = b H ⟺ a^{- 1} b \in H .$

The corresponding right-coset criterion is $H a = H b$ if and only if $a b^{- 1} \in H$ .

Facts & Assumptions

Given: A group $G$ , a subgroup $H \leq G$ , and elements $a, b, x \in G$ .

[F1]

The left coset $a H$ is ${a h : h \in H}$ , and the right coset $H a$ is ${h a : h \in H}$ (Left and right cosets $g H$ and $H g$ of a subgroup).

[F2]

A subgroup contains the identity and is closed under products and inverses (Subgroup).

[L1]

In a group, $(u v)^{- 1} = v^{- 1} u^{- 1}$ and $(u^{- 1})^{- 1} = u$ (In a group $e^{- 1} = e$ , $(g^{- 1})^{- 1} = g$ and $(g h)^{- 1} = h^{- 1} g^{- 1}$ , the order of the last product being essential).

[L2]

Left and right cancellation hold in every group (Cancellation in a group: $g x = g y$ or $x g = y g$ forces $x = y$ ; equivalently left and right translation by $g$ are bijections of $G$ , so $g x = h$ and $x g = h$ each have exactly one solution, Group and abelian group).

Proof

technique · direct

1.1F1F2L2

If $x \in a H$ , write $x = a h$ with $h \in H$ ; then $a^{- 1} x = a^{- 1} a h = h \in H$ . Conversely, if $a^{- 1} x \in H$ , then $x = a (a^{- 1} x) \in a H$ .

1.2givenF1F2

Suppose $a^{- 1} b \in H$ . If $x \in b H$ , write $x = b h = a (a^{- 1} b) h$ ; subgroup closure gives $(a^{- 1} b) h \in H$ , so $x \in a H$ . Thus $b H \subseteq a H$ .

2.1step 1.1F1F2

If $a H = b H$ , then $b = b e \in b H = a H$ , so step 1.1 gives $a^{- 1} b \in H$ .

2.2step 1.2F2L1

Since $(a^{- 1} b)^{- 1} = b^{- 1} a \in H$ , the same argument with $a, b$ interchanged gives $a H \subseteq b H$ . Hence $a H = b H$ .

3.1step 2.1step 1.2step 2.2F2L1∎

Finally, $H a = H b$ is equivalent, after taking inverses elementwise, to $a^{- 1} H = b^{- 1} H$ ; by the left-coset criterion this holds exactly when $a b^{- 1} \in H$ .

$x \in a H$ iff $a^{- 1} x \in H$ , and $a H = b H$ iff $a^{- 1} b \in H$

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

x∈aHx∈aH iff a−1x∈Ha−1x∈H, and aH=bHaH=bH iff a−1b∈Ha−1b∈H

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

$x \in a H$ iff $a^{- 1} x \in H$ , and $a H = b H$ iff $a^{- 1} b \in H$