WikiLeanRecent changes · Proposals · Flags · Stats · About

Diff — Determinant

Revision #1722 → #2224 · back to history

modifiedDeterminant as n-dimensional signed volumeaa85f068b1d9
FieldFrom #1722To #2224
mathlib.moduleMathlib.MeasureTheory.Measure.Haar.InnerProductSpaceMathlib.Analysis.InnerProductSpace.Orientation
modifiedDeterminant is homogeneousb0652f76a89b
FieldFrom #1722To #2224
anchors[{"section":"Immediate consequences","snippet":"The determinant is a homogeneous function"},{"type":"math_alttext","value":"{\\displaystyle \\det(cA)=c^{n}\\det(A)}"}]—
modifiedColumn swap multiplies determinant by −1d1bcd5492f7b
FieldFrom #1722To #2224
anchors[{"section":"Immediate consequences","snippet":"Interchanging any pair of columns of a matrix multiplies its determinant by"},{"type":"math_alttext","value":"{\\displaystyle |a_{1},\\dots ,a_{j},\\dots a_{i},\\dots ,a_{n}|=-|a_{1},\\dots ,a_{i},\\dots ,a_{j},\\dots ,a_{n}|.}"},{"type":"math_alttext","value":"{\\displaystyle |a_{3},a_{1},a_{2},a_{4}\\dots ,a_{n}|=-|a_{1},a_{3},a_{2},a_{4},\\dots ,a_{n}|=|a_{1},a_{2},a_{3},a_{4},\\dots ,a_{n}|.}"}]—
modifiedTriangular matrix determinant equals product of diagonal31d422a7fef4
FieldFrom #1722To #2224
anchors[{"section":"Immediate consequences","snippet":"its determinant equals the product of the diagonal entries"},{"type":"math_alttext","value":"{\\displaystyle \\det(A)=a_{11}a_{22}\\cdots a_{nn}=\\prod _{i=1}^{n}a_{ii}.}"}]—
modifiedMinor and cofactor of a matrixe6aff5bf20a1
FieldFrom #1722To #2224
mathlib.moduleMathlib.Data.Matrix.BasicMathlib.LinearAlgebra.Matrix.Defs
modifiedDeterminant inequality for positive semidefinite matricescab9aca640e2
FieldFrom #1722To #2224
anchors[{"section":"Sum","snippet":"for positive semidefinite matrices"},{"type":"math_alttext","value":"{\\displaystyle \\det(A+B+C)+\\det(C)\\geq \\det(A+C)+\\det(B+C){\\text{,}}}"},{"type":"math_alttext","value":"{\\displaystyle \\det(A+B)\\geq \\det(A)+\\det(B){\\text{.}}}"}]—
modifiedBrunn–Minkowski concavity of nth-root determinant315b55dbd260
FieldFrom #1722To #2224
anchors[{"section":"Sum","snippet":"Brunn–Minkowski theorem implies that the n th root of determinant is a concave function"},{"type":"math_alttext","value":"{\\displaystyle {\\sqrt[{n}]{\\det(A+B)}}\\geq {\\sqrt[{n}]{\\det(A)}}+{\\sqrt[{n}]{\\det(B)}},}"}]—
modifiedCross product as a formal 3×3 determinantc9543af48021
FieldFrom #1722To #2224
anchors[{"section":"Cross Product","snippet":"The computation of a cross product is equivalent to finding the formal determinant"},{"type":"math_alttext","value":"{\\displaystyle \\mathbf {a\\times b} =\\det {\\begin{pmatrix}\\mathbf {i} &\\mathbf {j} &\\mathbf {k} \\\\a_{1}&a_{2}&a_{3}\\\\b_{1}&b_{2}&b_{3}\\\\\\end{pmatrix}}}"}]—
modifiedJacobian matrix163417356030
FieldFrom #1722To #2224
mathlib.moduleMathlib.Analysis.Calculus.FDeriv.BasicMathlib.Analysis.Calculus.FDeriv.Defs
addedTrace equals sum of eigenvalues98ae323daf2e
addedSingularity iff zero is an eigenvalue02ede8094dec
addedQuotient GL/SL ≅ multiplicative group of units3acbad56df50