ExampleConstruction: Literature-sourcedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-28

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 quaternion group $Q_{8}$ acts on $H$ by left multiplication

Example

The quaternion group $Q_{8}$ acts on the real vector space $H$ by left multiplication: $q \cdot x : = q x (q \in Q_{8}, x \in H) .$ This is a $4$ -dimensional real representation of $Q_{8}$ .

Facts & Assumptions

Given: The quaternion group $Q_{8}$ and the quaternions $H$ .

[L1]

The group $Q_{8}$ is the subset ${\pm 1, \pm i, \pm j, \pm k}$ of the nonzero quaternions (The quaternion group $Q_{8} = {\pm 1, \pm i, \pm j, \pm k}$ inside the nonzero quaternions).

[L2]

The quaternions form a division ring, so multiplication is associative and every nonzero quaternion is invertible ( $H$ is a division ring that is not commutative, hence not a field: $q^{- 1} = \overset{ˉ}{q} / N (q)$ for $q \neq 0$ , while $i j = k$ and $j i = - k$ ).

[L3]

The quaternions are the real vector space $R^{4}$ with basis $1, i, j, k$ (The quaternions $H$ : real quadruples with componentwise addition and an explicit multiplication formula matching the table on $1, i, j, k$ ).

Verification

technique · direct

1.1

For each $q \in Q_{8}$ , define $L_{q} : H \to H$ by $L_{q} (x) = q x$ . By [L2], quaternion multiplication is distributive and real scalars commute with every quaternion, so $L_{q}$ is $R$ -linear. By [L3], the underlying vector space is $4$ -dimensional.

L2L3given

1.2

Because each $q \in Q_{8}$ is nonzero by [L1], [L2] gives an inverse $q^{- 1}$ in $H$ , and $L_{q^{- 1}}$ is the inverse of $L_{q}$ . So every $L_{q}$ is an invertible linear map.

L1L2

2.1

The action laws hold: $1 \cdot x = x$ , and $(p q) \cdot x = (p q) x = p (q x) = p \cdot (q \cdot x)$ by associativity from [L2]. Therefore left multiplication is a finite-dimensional real representation of $Q_{8}$ .

step 1.1step 1.2L2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

31 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

Peter Webb, A Course in Finite Group Representation Theory, Exercise 12 (standard reference, not scraped)

The quaternion group Q8Q8​ acts on HH by left multiplication