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.
One operator has matrices and in two bases, both with determinant
Example
Let on . In the standard ordered basis , its matrix is . In the ordered basis , its matrix is . Both determinants are .
Facts & Assumptions
Given: as in the example.
is a field (The reals form a field).
The determinant is the two-term Leibniz sum (For , the determinant over a commutative ring by the Leibniz formula, and for a real matrix).
The operator determinant is independent of the ordered basis (The determinant of a linear operator is independent of the chosen ordered basis).
Verification
Direct evaluation gives and , whose inverse is .
Matrix multiplication in [L1] gives
By the two-term determinant formula, and .
The explicit computations in steps 3.1 and 2.1 illustrate the equality asserted abstractly by [L2].
Depends on
- The determinant of a linear operator is independent of the chosen ordered basis
- $[T]_{\mathcal B'}^{\mathcal C'}=P_{\mathcal C'\leftarrow\mathcal C}[T]_{\mathcal B}^{\mathcal C}P_{\mathcal B\leftarrow\mathcal B'}$
- For $n\ge1$, the determinant over a commutative ring by the Leibniz formula, and $|\det A|$ for a real matrix
- The reals form a field
Used by
Nothing in the library uses this result yet.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 68 results over 15 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.