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 , the determinant over a commutative ring by the Leibniz formula, and for a real matrix
Definition
Let be a commutative ring, let , and let . Its determinant is The sum is finite because has elements. The product is taken in , so the signs and act through the ring identities. The formula uses columns indexed by and rows indexed by .
When is real, means the ordinary real absolute value of its real determinant. It is not alternate notation for the determinant itself.
Depends on
- Finite rectangular matrices over a commutative ring, their entries, rows and columns
- Inversions, inversion number, the sign $\operatorname{sgn}(\sigma)=(-1)^{\operatorname{inv}(\sigma)}$, and even and odd permutations
- A finite sum in a commutative monoid indexed by an arbitrary finite set
- The product $g_0 g_1 \cdots g_{n-1}$ of a finite list in a monoid, by recursion, with the empty product ($n = 0$) equal to the identity
- A finite set $A$ with $\lvert A\rvert = n$ has exactly $n!$ bijections onto itself, and $n!$ bijections onto any set of the same cardinality
- Absolute value in an ordered field
- The reals form a field
- The reals form a totally ordered field
- Every field is a commutative ring with $1 \ne 0$; it is an integral domain, and it is a commutative division ring
Used by
- For every fixed finite size at least one, the determinant of a real square matrix is a polynomial in its matrix entries Corollary
- The Jacobian determinant of a square-dimensional C¹ map is the determinant of its Jacobian matrix Definition
- A full 3×3 Leibniz expansion lists all six permutations and their signs Example
- For n≥ 1, determinant is a natural transformation det:GLₙ(-)⟹(-)^× from commutative rings to groups Example
- The content of a concrete three-dimensional parallelepiped computed from its spanning matrix Example
- The hyperspherical-coordinate Jacobian is the standard product of a radial power and sine powers Example
- The Leibniz formula gives detbeginpmatrixa&bc&d endpmatrix=ad-bc Example
- A linear endomorphism of ℝⁿ sends bounded Jordan sets to bounded Jordan sets and scales their content by the absolute determinant Theorem
- For every square matrix over a commutative ring, det(A^mathsf T)=det(A) Theorem
- For every square matrix, including singular ones, a row swap negates the determinant, scaling a row by any scalar scales it, and row addition leaves it unchanged Theorem
- For same-sized finite square matrices over a commutative ring, det(AB)=det(A)det(B) Theorem
- The determinant of a triangular matrix is the product of its diagonal entries Theorem
- The Leibniz determinant is column-multilinear, alternating and normalized over every commutative ring Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 108 results over 27 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.
Sources
- S. New, MATH 146 Linear Algebra 1 Lecture Notes, Definition 4.21 (standard reference, not scraped)
- P. Massot, Structures algébriques fondamentales, Definition 6.4.1 (standard reference, not scraped)
- D. Margalit and J. Rabinoff, Interactive Linear Algebra, §4.1 (standard reference, not scraped)