Alphabeta MathHow 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.
For symmetric with invertible, a block-unitriangular congruence gives and factors
Statement
Let
be symmetric over a field, with square diagonal blocks and invertible. Put . Then for
one has , and
where the determinant of a block is interpreted as .
Facts & Assumptions
Given: The displayed symmetric block matrix with invertible; an empty square block has determinant .
A basis change by changes a bilinear-form matrix to (A basis change by changes the matrix of a bilinear form from to ).
For a positive-sized square matrix over a commutative ring, the determinant is the signed sum over permutations of products selecting one entry in each row and column (For , the determinant over a commutative ring by the Leibniz formula, and for a real matrix).
Determinants of positive-sized square matrices over a commutative ring are multiplicative (For same-sized finite square matrices over a commutative ring, ).
A triangular matrix has determinant equal to the product of its diagonal entries (The determinant of a triangular matrix is the product of its diagonal entries).
Block products obey associative and distributive matrix arithmetic (Matrix arithmetic over a commutative ring is associative, unital and distributive, and transpose reverses products).
Proof
If the total size is zero, every block and is empty, both displayed matrix identities are the empty identity, and the determinant formula reads . Otherwise is block upper triangular with identity diagonal blocks, and ; hence it is invertible and [L4] gives .
Since symmetry of makes and therefore , direct multiplication gives .
In positive total size, [L3] and step 1.1 give . In the Leibniz sum [L2] for the block diagonal matrix of step 2.1, every nonzero term preserves both index blocks, so its determinant is , with the stated empty-block convention when one block has size zero. Thus .
The calculation proves both assertions. Zero-sized blocks, zero entries inside , and singular require no cancellation and are all included.
Depends on
- A basis change by $P$ changes the matrix of a bilinear form from $A$ to $P^{\mathsf T}AP$
- For $n\ge1$, the determinant over a commutative ring by the Leibniz formula, and $|\det A|$ for a real matrix
- For same-sized finite square matrices over a commutative ring, $\det(AB)=\det(A)\det(B)$
- The determinant of a triangular matrix is the product of its diagonal entries
- Matrix arithmetic over a commutative ring is associative, unital and distributive, and transpose reverses products
Used by
Dependency tree · two levels
24 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
- J. Kuan, Positive Definite Matrices (standard reference, not scraped)