PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-05

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.

Brackets of root spaces add their roots

Statement

Let $g = h \oplus ⨁_{α \in Φ} g_{α}$ be the decomposition from Root-space decomposition relative to a Cartan subalgebra. If $x \in g_{α}$ and $y \in g_{β}$ , then

$[x, y] \in g_{α + β},$

where $g_{0} : = h$ . In particular, if $α + β$ is neither $0$ nor a root, then $[x, y] = 0$ .

Facts & Assumptions

Given: Roots $α, β$ of a Cartan subalgebra $h$ and vectors $x \in g_{α}$ , $y \in g_{β}$ .

Proof

technique · direct

1.1

For every $h \in h$ , the derivation property of $ad (h)$ gives $[h, [x, y]] = [ad (h) x, y] + [x, ad (h) y] = α (h) [x, y] + β (h) [x, y] = (α + β) (h) [x, y]$ .

givenalgebra

2.1

By Root-space decomposition relative to a Cartan subalgebra, step 1.1 is exactly the defining condition for $[x, y]$ to lie in the root space with weight $α + β$ . If that root space is zero, then $[x, y] = 0$ .

step 1.1∎

Depends on

Root-space decomposition relative to a Cartan subalgebra

Used by

Dependency tree · two levels

2 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

Pavel Etingof, Lie Groups and Lie Algebras I (standard reference, not scraped)