theorem 15.54 Completeness in the bilinear case

open in the book · parts/02-mathematical-methods/13-lie-algebra-expansions.tex:2071 · p. 623

Rests on

depends_on definition 15.3 Tensor product Lie algebra ¶
depends_on lemma A.63 The invariant bilinear forms of an absolutely simple algebra form a line ¶
- depends_on definition A.62 Absolutely simple ¶
- proves proof app:A-long-proofs@proof-48 ¶
depends_on lemma 15.50 Every $k$-trace comes from a linear functional ¶
- depends_on definition 15.49 $k$-trace ¶
- proves proof ch:13-lie-algebra-expansions@proof-29 ¶
proves proof ch:13-lie-algebra-expansions@prooflink-1 ¶

Supports

depends_on definition 15.66 Gram form of a functional ¶
- depends_on corollary 15.70 Signature of the factorised form ¶
- depends_on lemma 15.67 Multiplication is $B_{\psi}$-self-adjoint ¶
  - depends_on theorem 15.68 Positive Gram forms are positive sums of real characters ¶
    - depends_on corollary 15.69 No positive pairing survives the radical ¶
- depends_on theorem 15.68 Positive Gram forms are positive sums of real characters ¶ ↺

Neighborhood

Every logical edge within two steps of this node.

declared and complete
partly declared
a check failed
not graded
declared in the source
inferred from structure

Edges

type	direction	node	provenance	where
`depends_on`	→	Tensor product Lie algebra	declared	parts/02-mathematical-methods/13-lie-algebra-expansions.tex:2083
`depends_on`	→	The invariant bilinear forms of an absolutely simple algebra form a line	declared	parts/02-mathematical-methods/13-lie-algebra-expansions.tex:2083
`depends_on`	→	Every $k$-trace comes from a linear functional	declared	parts/02-mathematical-methods/13-lie-algebra-expansions.tex:2083
`depends_on`	←	Gram form of a functional	declared	parts/02-mathematical-methods/13-lie-algebra-expansions.tex:2457
`proves`	←	ch:13-lie-algebra-expansions@prooflink-1	declared	parts/02-mathematical-methods/13-lie-algebra-expansions.tex:2085