ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-11

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.

Left multiplication gives a free and transitive action of every group on itself

Example

Every group $G$ acts on its underlying set by left multiplication, $g \cdot x = g x$ . This left regular action is free and transitive, and every stabilizer is the trivial subgroup.

Facts & Assumptions

Given: A group $G$ acting on its underlying set by $g \cdot x = g x$ .

[L1]

A left action satisfies $e \cdot x = x$ and $(g h) \cdot x = g \cdot (h \cdot x)$ and is transitive when some group element carries any point to any other (Left group actions, transitive actions, and faithful actions).

[L2]

An action is free when $g \cdot x = x$ implies $g = e$ (A free group action has no nonidentity element fixing a point).

[L3]

The stabilizer is $G_{x} = {g : g \cdot x = x}$ (The orbit $G \cdot x$ and stabilizer $G_{x}$ of a point in a group action).

Verification

technique · direct

1.1

The identities $e \cdot x = e x = x$ and $(g h) \cdot x = (g h) x = g (h x) = g \cdot (h \cdot x)$ verify the action laws.

L1algebra

2.1

Given $x, y \in G$ , the element $g = y x^{- 1}$ satisfies $g \cdot x = y$ , so the action is transitive.

step 1.1L1choosealgebra

3.1

If $g \cdot x = x$ , then $g x = x$ and right cancellation gives $g = e$ ; by [L2] the action is free, and [L3] gives $G_{x} = {e}$ for every $x$ .

step 1.1L2L3algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

4 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

T. W. Judson, Abstract Algebra: Theory and Applications, 14.1 (standard reference, not scraped)