Revision #1395 → #1841 · back to history
modifiedMatrix54f4ca67ae22
| Field | From #1395 | To #1841 |
|---|
| note | Mathlib defines `Matrix m n α := m → n → α`, matching the rectangular-array notion with arbitrary entry type. | `Matrix m n α := m → n → α` encodes the rectangular-array notion with arbitrary entry type. |
modified2×3 matrix examplef194fd16019c
| Field | From #1395 | To #1841 |
|---|
| anchors | [{"section":"(Lead)","snippet":"denotes a matrix with two rows and three columns"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{bmatrix}1&9&-13\\\\20&5&-6\\end{bmatrix}}}"}] | — |
| note | A concrete 2×3 example matrix is not part of Mathlib's library. | No concrete 2×3 illustrative matrix is part of Mathlib's library. |
modifiedSquare matrix (lead)a16c309ee753
| Field | From #1395 | To #1841 |
|---|
| note | Square matrices are written as `Matrix n n α` (same index type for rows and columns); there is no separate `SquareMatrix` definition. | Square matrices are written `Matrix n n α` (same index type on both sides); there is no separate `SquareMatrix` definition. |
modifiedInvertibility and determinant0ee8254f9279
| Field | From #1395 | To #1841 |
|---|
| note | Mathlib proves `IsUnit A ↔ IsUnit A.det` over a commutative ring; over a field this reduces to det ≠ 0. | `Matrix.isUnit_iff_isUnit_det` states `IsUnit A ↔ IsUnit A.det` over a commutative ring; over a field this reduces to det ≠ 0. |
modifiedMatrix (formal)b1898e6579d6
| Field | From #1395 | To #1841 |
|---|
| anchors | [{"section":"Definition","snippet":"A matrix is a rectangular array of numbers (or other mathematical objects), called the \"entries\""},{"type":"math_alttext","value":"{\\displaystyle \\mathbf {A} ={\\begin{bmatrix}-1.3&0.6\\\\20.4&5.5\\\\9.7&-6.2\\end{bmatrix}}.}"}] | — |
| note | Same `Matrix` definition encodes the formal rectangular-array notion. | The same `Matrix` definition encodes the formal rectangular-array notion. |
modifiedReal and complex matrixc3cb62f0d311
| Field | From #1395 | To #1841 |
|---|
| anchors | [{"section":"Definition","snippet":"A real matrix and a complex matrix are matrices whose entries are respectively real numbers or complex numbers"},{"type":"math_alttext","value":"{\\displaystyle \\mathbf {A} ={\\begin{bmatrix}-1.3&0.6\\\\20.4&5.5\\\\9.7&-6.2\\end{bmatrix}}.}"}] | — |
| note | Real/complex matrices are instances `Matrix m n ℝ` / `Matrix m n ℂ`; no dedicated abbreviations. | Real/complex matrices are simply `Matrix m n ℝ` / `Matrix m n ℂ`; no dedicated abbreviation. |
modifiedRows and columns38871bb2f26f
| Field | From #1395 | To #1841 |
|---|
| note | Matrices are indexed by row/column types and `Matrix.row`/`Matrix.col` extract row/column functions. | Matrices are indexed by row/column types; `Matrix.row`/`Matrix.col` package row and column functions. |
| provenance | ai | ai-moderated |
modifiedSize of a matrixa6de1942e258
| Field | From #1395 | To #1841 |
|---|
| note | Size is encoded by the index types `m` and `n`; no explicit `size` function is defined. | Size is encoded by the index types `m` and `n` themselves; there is no explicit `size` function. |
modifiedm × n matrix036cf8fe82bf
| Field | From #1395 | To #1841 |
|---|
| note | Expressed as `Matrix (Fin m) (Fin n) α`; no separate `mxnMatrix` abbreviation. | Expressed as `Matrix (Fin m) (Fin n) α`; no dedicated abbreviation. |
modifiedRow and column vectors5d184a6deba0
| Field | From #1395 | To #1841 |
|---|
| note | Row/column vectors are typically written as `Matrix Unit n α` or via `Matrix.row`/`Matrix.col`; no separate named type. | Row/column vectors are written via `Matrix.row`/`Matrix.col` or as `Matrix Unit n α`; no separate named type. |
| provenance | ai | ai-moderated |
modifiedSquare matrix5d29907d84ee
| Field | From #1395 | To #1841 |
|---|
| note | Square matrices are written `Matrix n n α`; no dedicated wrapper type. | Square matrices are `Matrix n n α`; no dedicated wrapper type. |
modifiedInfinite matrix0a51cecb02d5
| Field | From #1395 | To #1841 |
|---|
| note | Mathlib's `Matrix m n α` allows arbitrary (including infinite) index types, but many operations (mul, det) require `Fintype`. | `Matrix m n α` allows arbitrary (including infinite) index types, but most operations like `mul`/`det` require `Fintype`. |
modifiedMatrix addition and subtractiond380f4327656
| Field | From #1395 | To #1841 |
|---|
| mathlib.decl | Matrix.add | Matrix.add_apply |
| note | Entrywise `Add`, `Sub`, `Neg` instances on `Matrix m n α` are defined inheriting from the pi type. | `Add`/`Sub`/`Neg` instances on `Matrix m n α` inherited pointwise; `Matrix.add_apply` says `(A + B) i j = A i j + B i j`. |
| provenance | ai | ai-moderated |
modifiedCommutativity of matrix addition642ec7e4865d
| Field | From #1395 | To #1841 |
|---|
| note | The `AddCommMonoid (Matrix m n α)` instance gives commutativity of matrix addition. | The `AddCommMonoid (Matrix m n α)` instance `Matrix.addCommMonoid` gives commutativity of matrix addition. |
| provenance | ai | ai-moderated |
modifiedScalar multiplicationf0ebcb652f05
| Field | From #1395 | To #1841 |
|---|
| anchors | [{"section":"Scalar multiplication","snippet":"The product c A of a number c (also called a scalar in this context) and a matrix A is computed by multiplying each entry of A by c"},{"type":"math_alttext","value":"{\\displaystyle (c{\\mathbf {A}})_{i,j}=c\\cdot {\\mathbf {A}}_{i,j}}"}] | — |
| mathlib.decl | Matrix.smul | Matrix.smul_apply |
| note | Entrywise `SMul R (Matrix m n α)` instance encodes scalar multiplication. | Pointwise `SMul R (Matrix m n α)`; `(c • A) i j = c • A i j` via `Matrix.smul_apply`. |
| provenance | ai | ai-moderated |
modifiedTranspose9cbc6dc2c56b
| Field | From #1395 | To #1841 |
|---|
| anchors | [{"section":"Transpose","snippet":"The transpose of an m × n matrix A is the n × m matrix A T (also denoted A tr or t A ) formed by turning rows into columns and vice versa"},{"type":"math_alttext","value":"{\\displaystyle \\left({\\mathbf {A}}^{\\rm {T}}\\right)_{i,j}={\\mathbf {A}}_{j,i}.}"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{bmatrix}1&2&3\\\\0&-6&7\\end{bmatrix}}^{\\mathrm {T} }={\\begin{bmatrix}1&0\\\\2&-6\\\\3&7\\end{bmatrix}}}"}] | — |
| note | `Matrix.transpose M i j = M j i`, notated `Mᵀ`. | `Matrix.transpose M i j = M j i`, with notation `Mᵀ`. |
| provenance | ai | ai-moderated |
modifiedTranspose propertiese91ad0076b40
| Field | From #1395 | To #1841 |
|---|
| note | `Matrix.transpose_add`, `transpose_smul`, `transpose_mul` are all in Mathlib. | `Matrix.transpose_add`, `transpose_smul`, `transpose_transpose`, and `transpose_mul` are in Mathlib. |
| provenance | ai | ai-moderated |
modifiedMatrix multiplication2a51ee03de50
| Field | From #1395 | To #1841 |
|---|
| anchors | [{"section":"Matrix multiplication","snippet":"If A is an m × n matrix and B is an n × p matrix, then their matrix product AB is the m × p matrix"},{"type":"math_alttext","value":"{\\displaystyle [\\mathbf {AB} ]_{i,j}=a_{i,1}b_{1,j}+a_{i,2}b_{2,j}+\\cdots +a_{i,n}b_{n,j}=\\sum _{r=1}^{n}a_{i,r}b_{r,j},}"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}{\\begin{bmatrix}{\\underline {2}}&{\\underline {3}}&{\\underline {4}}\\\\1&0&0\\\\\\end{bmatrix}}{\\begin{bmatrix}0&{\\underline {1000}}\\\\1&{\\underline {100}}\\\\0&{\\underline {10}}\\\\\\end{bmatrix}}&={\\begin{bmatrix}3&{\\underline {2340}}\\\\0&1000\\\\\\end{bmatrix}}.\\end{aligned}}}"}] | — |
| mathlib.decl | Matrix.mul | Matrix.mul_apply |
| note | Matrix multiplication is defined via `HMul`/`Mul` instances on `Matrix m n α` × `Matrix n p α`. | Matrix multiplication is defined via the `HMul` instance and characterized by `Matrix.mul_apply : (A * B) i j = ∑ k, A i k * B k j`. |
modifiedAssociativity and distributivity of matrix multiplication9006505832d9
| Field | From #1395 | To #1841 |
|---|
| anchors | [{"section":"Matrix multiplication","snippet":"Matrix multiplication satisfies the rules"},{"type":"math_alttext","value":"{\\displaystyle {\\mathbf {AB}}\\neq {\\mathbf {BA}}.}"}] | — |
| note | `Matrix.mul_assoc` and the `NonUnitalNonAssocSemiring`/`Semiring` instances yield distributivity. | `Matrix.mul_assoc` plus the `NonUnitalNonAssocSemiring`/`Semiring` instances yield associativity and distributivity. |
modifiedNon-commutativity of matrix multiplicationb60c2569994a
| Field | From #1395 | To #1841 |
|---|
| anchors | [{"section":"Matrix multiplication","snippet":"matrix multiplication is not commutative , in marked contrast to (rational, real, or complex) numbers"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{bmatrix}1&2\\\\3&4\\\\\\end{bmatrix}}{\\begin{bmatrix}0&1\\\\0&0\\\\\\end{bmatrix}}={\\begin{bmatrix}0&1\\\\0&3\\\\\\end{bmatrix}},}"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{bmatrix}0&1\\\\0&0\\\\\\end{bmatrix}}{\\begin{bmatrix}1&2\\\\3&4\\\\\\end{bmatrix}}={\\begin{bmatrix}3&4\\\\0&0\\\\\\end{bmatrix}}.}"}] | — |
| note | No explicit Mathlib lemma asserting non-commutativity of matrix multiplication (it is implicit in the lack of `CommRing` instance). | No explicit Mathlib lemma asserts non-commutativity (it is implicit in the absence of a `CommRing` instance). |
addedHadamard product29e4e760a7d5
addedKronecker product35883cd03adb
modifiedRow operationsb85a2227d8dd
| Field | From #1395 | To #1841 |
|---|
| mathlib.module | Mathlib.Data.Matrix.RowCol | Mathlib.LinearAlgebra.Matrix.RowCol |
| note | Mathlib has `Matrix.updateRow`, `Matrix.transvection`, and row swapping but no single unified "elementary row operation" classifier. | Mathlib has `Matrix.updateRow`, `Matrix.transvection`, and row-swap operations, but no unified "elementary row operation" classifier. |
modifiedSubmatrixe0c353ef7fe1
| Field | From #1395 | To #1841 |
|---|
| anchors | [{"section":"Submatrix","snippet":"A submatrix of a matrix is a matrix obtained by deleting any collection of rows or columns or both"},{"type":"math_alttext","value":"{\\displaystyle \\mathbf {A} ={\\begin{bmatrix}1&\\color {red}{2}&3&4\\\\5&\\color {red}{6}&7&8\\\\\\color {red}{9}&\\color {red}{10}&\\color {red}{11}&\\color {red}{12}\\end{bmatrix}}\\rightarrow {\\begin{bmatrix}1&3&4\\\\5&7&8\\end{bmatrix}}.}"}] | — |
| note | `Matrix.submatrix A r c` reindexes rows/columns by arbitrary functions, subsuming the row/column-deletion view. | `Matrix.submatrix A r c` reindexes rows/columns by arbitrary functions, subsuming row/column deletion. |
| provenance | ai | ai-moderated |
modifiedPrincipal submatrixf4a7fd82659d
| Field | From #1395 | To #1841 |
|---|
| note | Expressible as `M.submatrix f f` but there is no `principalSubmatrix` definition. | Expressible as `M.submatrix f f` but there is no dedicated `principalSubmatrix` definition. |
| provenance | ai | ai-moderated |
modifiedMatrix equation for linear systems02586494e340
| Field | From #1395 | To #1841 |
|---|
| anchors | [{"section":"Linear equations","snippet":"Matrices can be used to compactly write and work with multiple linear equations"},{"type":"math_alttext","value":"{\\displaystyle \\mathbf {Ax} =\\mathbf {b} }"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}a_{1,1}x_{1}+a_{1,2}x_{2}+&\\cdots +a_{1,n}x_{n}=b_{1}\\\\&\\ \\ \\vdots \\\\a_{m,1}x_{1}+a_{m,2}x_{2}+&\\cdots +a_{m,n}x_{n}=b_{m}\\end{aligned}}}"}] | — |
| note | Linear systems are written `A *ᵥ x = b` via `Matrix.mulVec`; no dedicated `LinearSystem` notion. | Linear systems are written `A *ᵥ x = b` via `Matrix.mulVec`; there is no dedicated `LinearSystem` notion. |
modifiedSolution via inverse matrix8fe88448251a
| Field | From #1395 | To #1841 |
|---|
| anchors | [{"section":"Linear equations","snippet":"If n = m and the equations are independent , then this can be done by writing"},{"type":"math_alttext","value":"{\\displaystyle \\mathbf {x} =\\mathbf {A} ^{-1}\\mathbf {b} }"}] | — |
| note | Mathlib provides `A⁻¹` (`nonsing_inv`) and `A * A⁻¹ = 1` results, from which `x = A⁻¹ *ᵥ b` follows, but the explicit system-solution statement is not a single lemma. | Mathlib provides `A⁻¹` (`nonsing_inv`) and `A * A⁻¹ = 1`, from which `x = A⁻¹ *ᵥ b` follows; not packaged as a single lemma. |
modifiedLinear transformation from matrixe49aa91140be
| Field | From #1395 | To #1841 |
|---|
| note | `Matrix.toLin'` is the linear-equivalence `Matrix m n R ≃ₗ[R] (n → R) →ₗ[R] (m → R)`. | `Matrix.toLin'` is the linear equivalence `Matrix m n R ≃ₗ[R] (n → R) →ₗ[R] (m → R)`. |
modified2×2 matrix as parallelogram transform8bba182ae8ed
| Field | From #1395 | To #1841 |
|---|
| anchors | [{"section":"Linear transformations","snippet":"the 2 × 2 matrix [MATH] can be viewed as the transform of the unit square into a parallelogram"},{"type":"math_alttext","value":"{\\displaystyle \\mathbf {A} ={\\begin{bmatrix}a&c\\\\b&d\\end{bmatrix}}}"}] | — |
| note | The geometric parallelogram-image example is not part of Mathlib. | The geometric parallelogram-image example is not present in Mathlib. |
modifiedMatrix multiplication as composition849ce0a05335
| Field | From #1395 | To #1841 |
|---|
| anchors | [{"section":"Linear transformations","snippet":"Under the 1-to-1 correspondence between matrices and linear maps, matrix multiplication corresponds to composition of maps"},{"type":"math_alttext","value":"{\\displaystyle (g\\circ f)({\\mathbf {x}})=g(f({\\mathbf {x}}))=g({\\mathbf {Ax}})={\\mathbf {B}}({\\mathbf {Ax}})=({\\mathbf {BA}}){\\mathbf {x}}.}"}] | — |
modifiedRank of a matrixec94475a778a
| Field | From #1395 | To #1841 |
|---|
| note | `Matrix.rank` is defined and `rank_eq_finrank_span_cols`/`rank_eq_finrank_span_row` equate it with row/column rank. | `Matrix.rank` is defined and equated with row/column rank by `rank_eq_finrank_span_*` lemmas. |
modifiedRank–nullity theorem193f4d7b2479
| Field | From #1395 | To #1841 |
|---|
| note | Rank-nullity is `LinearMap.finrank_range_add_finrank_ker`, used in `Matrix/Rank.lean` for matrices via `toLin`. | Rank–nullity is `LinearMap.finrank_range_add_finrank_ker`, used for matrices via `toLin`. |
modifiedSquare matrix and main diagonal172ffd5985c2
| Field | From #1395 | To #1841 |
|---|
| note | Square matrices are `Matrix n n α`; main diagonal is `Matrix.diag`. | Square matrices are `Matrix n n α`; the main diagonal is `Matrix.diag`. |
modifiedSquare matrices form noncommutative ring151de3550ee5
| Field | From #1395 | To #1841 |
|---|
| note | `instance instRing : Ring (Matrix n n α)` for `Fintype n` and `Ring α`. | `Matrix.instRing` provides `Ring (Matrix n n α)` for `Fintype n` and `Ring α`. |
modifiedTriangular and diagonal matricesf004ab528ddc
| Field | From #1395 | To #1841 |
|---|
| note | `Matrix.BlockTriangular` (and `Matrix.IsDiag` for diagonal) generalize triangular matrices; no specific `IsUpperTriangular` predicate. | `Matrix.BlockTriangular` generalizes triangular matrices, and `Matrix.IsDiag` handles diagonal ones; no dedicated `IsUpperTriangular` predicate. |
addedDiagonal matrixe932cda0449a
modifiedIdentity matrix99cdec511e42
| Field | From #1395 | To #1841 |
|---|
| anchors | [{"section":"Identity matrix","snippet":"The identity matrix I n of size n is the n -by- n matrix in which all the elements on the main diagonal are equal to 1"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}\\mathbf {I} _{1}&={\\begin{bmatrix}1\\end{bmatrix}},\\\\[4pt]\\mathbf {I} _{2}&={\\begin{bmatrix}1&0\\\\0&1\\end{bmatrix}},\\\\[4pt]\\vdots &\\\\[4pt]\\mathbf {I} _{n}&={\\begin{bmatrix}1&0&\\cdots &0\\\\0&1&\\cdots &0\\\\\\vdots &\\vdots &\\ddots &\\vdots \\\\0&0&\\cdots &1\\end{bmatrix}}\\end{aligned}}}"},{"type":"math_alttext","value":"{\\displaystyle {\\mathbf {AI}}_{n}={\\mathbf {I}}_{m}{\\mathbf {A}}={\\mathbf {A}}}"}] | — |
| note | `instance one : One (Matrix n n α) := ⟨diagonal fun _ => 1⟩` gives the identity matrix `1`. | The `One (Matrix n n α)` instance is `Matrix.one`, defined as `diagonal fun _ => 1`. |
modifiedScalar matrixe19839c4bd62
| Field | From #1395 | To #1841 |
|---|
| note | Mathlib has `Matrix.diagonalRingHom`/`scalar` (sending `r` to `r • 1` as a ring hom) but no `IsScalarMatrix` predicate. | `Matrix.scalar` is the ring hom sending `r` to `r • 1`; there is no `IsScalarMatrix` predicate. |
| provenance | ai | ai-moderated |
modifiedSymmetric and skew-symmetric matricesc3db72c83a16
| Field | From #1395 | To #1841 |
|---|
| note | `Matrix.IsSymm A := Aᵀ = A` is defined; no separate `IsSkewSymm` predicate, though `-A = Aᵀ` is expressible. | `Matrix.IsSymm A := Aᵀ = A` is defined; there is no dedicated `IsSkewSymm` predicate. |
addedConjugate transpose4986cdf75499
modifiedInvertible matrixe5657cf57756
| Field | From #1395 | To #1841 |
|---|
| anchors | [{"section":"Invertible matrix and its inverse","snippet":"A square matrix A is called invertible or non-singular if there exists a matrix B such that"},{"type":"math_alttext","value":"{\\displaystyle {\\mathbf {AB}}={\\mathbf {BA}}={\\mathbf {I}}_{n},}"}] | — |
| note | Invertibility is `IsUnit A` in the matrix ring; characterized by `isUnit_iff_isUnit_det` and `Matrix.invertibleOfDetInvertible`. | Invertibility is `IsUnit A` in the matrix ring, characterized by `Matrix.isUnit_iff_isUnit_det`. |
modifiedUniqueness of inverse05cbf5e15269
| Field | From #1395 | To #1841 |
|---|
| anchors | [{"section":"Invertible matrix and its inverse","snippet":"If B exists, it is unique and is called the inverse matrix of A"},{"type":"math_alttext","value":"{\\displaystyle {\\mathbf {AB}}={\\mathbf {BA}}={\\mathbf {I}}_{n},}"}] | — |
| note | Uniqueness follows from `Group`/`Units` structure on the matrix ring; the chosen inverse is `A⁻¹` (`nonsing_inv`). | Uniqueness follows from the `Units`/`Group` structure on the matrix ring; the chosen inverse is `A⁻¹` (`nonsing_inv`). |
modifiedPositive-definite and indefinite matrices449d06e6ec56
| Field | From #1395 | To #1841 |
|---|
| anchors | [{"section":"Definite matrix","snippet":"A symmetric real matrix A is called positive-definite if the associated quadratic form"},{"type":"math_alttext","value":"{\\displaystyle f({\\mathbf {x}})={\\mathbf {x}}^{\\rm {T}}{\\mathbf {Ax}}}"}] | — |
modifiedBilinear form associated to matrix9ff2c8d10889
| Field | From #1395 | To #1841 |
|---|
| anchors | [{"section":"Definite matrix","snippet":"Allowing as input two different vectors instead yields the bilinear form associated to A"},{"type":"math_alttext","value":"{\\displaystyle B_{\\mathbf {A}}({\\mathbf {x}},{\\mathbf {y}})={\\mathbf {x}}^{\\rm {T}}{\\mathbf {Ay}}.}"}] | — |
| note | `Matrix.toBilin'` is the linear equivalence `Matrix n n R₁ ≃ₗ BilinForm R₁ (n → R₁)`. | `Matrix.toBilin'` is the linear equivalence between `Matrix n n R₁` and bilinear forms on `n → R₁`. |
modifiedOrthogonal matrix5662ef824bda
| Field | From #1395 | To #1841 |
|---|
| anchors | [{"section":"Orthogonal matrix","snippet":"An orthogonal matrix is a square matrix with real entries whose columns and rows are orthogonal unit vectors"},{"type":"math_alttext","value":"{\\displaystyle \\mathbf {A} ^{\\mathrm {T} }=\\mathbf {A} ^{-1},\\,}"},{"type":"math_alttext","value":"{\\displaystyle \\mathbf {A} ^{\\mathrm {T} }\\mathbf {A} =\\mathbf {A} \\mathbf {A} ^{\\mathrm {T} }=\\mathbf {I} _{n},}"}] | — |
| note | `Matrix.orthogonalGroup n R := unitaryGroup n R`; `mem_orthogonalGroup_iff` says `A * Aᵀ = 1`. | `Matrix.orthogonalGroup n R := unitaryGroup n R`; membership is characterized by `A * Aᵀ = 1`. |
modifiedOrthogonal matrix properties9903a005b417
| Field | From #1395 | To #1841 |
|---|
| note | Orthogonal group is a `Group`, so each element is invertible; no dedicated lemma `IsOrthogonal.invertible`. | Orthogonal group is a `Group` so each element is invertible; no dedicated `IsOrthogonal.invertible` lemma. |
modifiedSpecial orthogonal matrixb9f942c0e016
| Field | From #1395 | To #1841 |
|---|
| note | `Matrix.specialOrthogonalGroup`, characterized as orthogonal matrices with `det = 1`. | `Matrix.specialOrthogonalGroup` is exactly orthogonal matrices with `det = 1`. |
addedUnitary matrixabc5e6fa4d19
modifiedTrace of a matrixa6412475bf40
| Field | From #1395 | To #1841 |
|---|
| anchors | [{"section":"Trace","snippet":"The trace , tr( A ) of a square matrix A is the sum of its diagonal entries"},{"type":"math_alttext","value":"{\\displaystyle \\operatorname {tr} (\\mathbf {AB} )=\\operatorname {tr} (\\mathbf {BA} ).}"},{"type":"math_alttext","value":"{\\displaystyle \\operatorname {tr} (\\mathbf {AB} )=\\sum _{i=1}^{m}\\sum _{j=1}^{n}a_{ij}b_{ji}=\\operatorname {tr} (\\mathbf {BA} ).}"},{"type":"math_alttext","value":"{\\displaystyle \\operatorname {tr} ({\\mathbf {A}})=\\operatorname {tr} ({\\mathbf {A}}^{\\rm {T}}).}"}] | — |
modifiedTrace of product independent of order27667fec90ae
| Field | From #1395 | To #1841 |
|---|
| anchors | [{"section":"Trace","snippet":"the trace of the product of two matrices is independent of the order of the factors"},{"type":"math_alttext","value":"{\\displaystyle \\operatorname {tr} (\\mathbf {AB} )=\\operatorname {tr} (\\mathbf {BA} ).}"},{"type":"math_alttext","value":"{\\displaystyle \\operatorname {tr} (\\mathbf {AB} )=\\sum _{i=1}^{m}\\sum _{j=1}^{n}a_{ij}b_{ji}=\\operatorname {tr} (\\mathbf {BA} ).}"},{"type":"math_alttext","value":"{\\displaystyle \\operatorname {tr} ({\\mathbf {A}})=\\operatorname {tr} ({\\mathbf {A}}^{\\rm {T}}).}"}] | — |
modifiedTrace equals trace of transpose70c0ba68f369
| Field | From #1395 | To #1841 |
|---|
| anchors | [{"section":"Trace","snippet":"the trace of a matrix is equal to that of its transpose"},{"type":"math_alttext","value":"{\\displaystyle \\operatorname {tr} (\\mathbf {AB} )=\\operatorname {tr} (\\mathbf {BA} ).}"},{"type":"math_alttext","value":"{\\displaystyle \\operatorname {tr} (\\mathbf {AB} )=\\sum _{i=1}^{m}\\sum _{j=1}^{n}a_{ij}b_{ji}=\\operatorname {tr} (\\mathbf {BA} ).}"},{"type":"math_alttext","value":"{\\displaystyle \\operatorname {tr} ({\\mathbf {A}})=\\operatorname {tr} ({\\mathbf {A}}^{\\rm {T}}).}"}] | — |
modifiedInvertibility iff nonzero determinant78ddf4d16ba9
| Field | From #1395 | To #1841 |
|---|
| note | `isUnit_iff_isUnit_det` over a `CommRing`; for fields `IsUnit ↔ ≠ 0`. | `Matrix.isUnit_iff_isUnit_det` over a `CommRing`; specializes to `det ≠ 0` over a field. |
modifiedDeterminant of 2×2 matrixd6095dd925ec
| Field | From #1395 | To #1841 |
|---|
| anchors | [{"section":"Determinant","snippet":"The determinant of 2 × 2 matrices is given by"},{"type":"math_alttext","value":"{\\displaystyle \\det {\\begin{bmatrix}a&b\\\\c&d\\end{bmatrix}}=ad-bc.}"}] | — |
addedLeibniz formula for determinant0d07fdb6e0f6
modifiedMultiplicativity of determinant54ea5be02b8b
| Field | From #1395 | To #1841 |
|---|
| anchors | [{"section":"Determinant","snippet":"The determinant of a product of square matrices equals the product of their determinants"},{"type":"math_alttext","value":"{\\displaystyle \\det({\\mathbf {AB}})=\\det({\\mathbf {A}})\\cdot \\det({\\mathbf {B}}),}"},{"type":"math_alttext","value":"{\\displaystyle |{\\mathbf {AB}}|=|{\\mathbf {A}}|\\cdot |{\\mathbf {B}}|.}"}] | — |
modifiedLaplace expansion71f3054f1f9a
| Field | From #1395 | To #1841 |
|---|
| anchors | [{"section":"Determinant","snippet":"the Laplace expansion expresses the determinant in terms of minors"},{"type":"math_alttext","value":"{\\displaystyle \\det({\\mathbf {AB}})=\\det({\\mathbf {A}})\\cdot \\det({\\mathbf {B}}),}"},{"type":"math_alttext","value":"{\\displaystyle |{\\mathbf {AB}}|=|{\\mathbf {A}}|\\cdot |{\\mathbf {B}}|.}"}] | — |
modifiedCramer's ruleff8ff5395d88
| Field | From #1395 | To #1841 |
|---|
| anchors | [{"section":"Determinant","snippet":"Determinants can be used to solve linear systems using Cramer's rule"},{"type":"math_alttext","value":"{\\displaystyle \\det({\\mathbf {AB}})=\\det({\\mathbf {A}})\\cdot \\det({\\mathbf {B}}),}"},{"type":"math_alttext","value":"{\\displaystyle |{\\mathbf {AB}}|=|{\\mathbf {A}}|\\cdot |{\\mathbf {B}}|.}"}] | — |
| note | `Matrix.cramer` and related lemmas (`cramer_apply`, `mul_adjugate`) encode Cramer's rule. | `Matrix.cramer`, with `cramer_apply` and `mul_adjugate`, encodes Cramer's rule. |
modifiedEigenvalue and eigenvector6bbe2ef36fba
| Field | From #1395 | To #1841 |
|---|
| anchors | [{"section":"Eigenvalues and eigenvectors","snippet":"are called an eigenvalue and an eigenvector of A , respectively"},{"type":"math_alttext","value":"{\\displaystyle \\mathbf {A} \\mathbf {v} =\\lambda \\mathbf {v} }"}] | — |
| note | `Module.End.HasEigenvalue` and `HasEigenvector` are defined for endomorphisms; applied to matrices via `Matrix.toLin`. | `Module.End.HasEigenvalue`/`HasEigenvector` are defined for endomorphisms and applied to matrices via `Matrix.toLin`. |
modifiedCharacteristic polynomial33dd341a2ac9
| Field | From #1395 | To #1841 |
|---|
| anchors | [{"section":"Eigenvalues and eigenvectors","snippet":"is called the characteristic polynomial of A"},{"type":"math_alttext","value":"{\\displaystyle \\mathbf {A} \\mathbf {v} =\\lambda \\mathbf {v} }"}] | — |
modifiedCayley–Hamilton theorem92a98da8a136
| Field | From #1395 | To #1841 |
|---|
| anchors | [{"section":"Eigenvalues and eigenvectors","snippet":"According to the Cayley–Hamilton theorem , p A ( A ) = 0"},{"type":"math_alttext","value":"{\\displaystyle \\mathbf {A} \\mathbf {v} =\\lambda \\mathbf {v} }"}] | — |
addedCharpoly is monic of degree n5b6c3955e1e8
modifiedStrassen algorithm complexityfdb766c2ed50
| Field | From #1395 | To #1841 |
|---|
| note | The Strassen matrix-multiplication algorithm and its complexity are not formalized in Mathlib. | Strassen's matrix-multiplication algorithm and its complexity are not formalized in Mathlib. |
modifiedSparse matrix8a5401d592a4
| Field | From #1395 | To #1841 |
|---|
| note | No notion of sparse matrices is in Mathlib. | No notion of sparse matrices exists in Mathlib. |
addedAdjugate matrixf07304f8e22d
modifiedSingular value decomposition8b03425ff04d
| Field | From #1395 | To #1841 |
|---|
| note | SVD is not formalized for matrices in Mathlib (only related notions like singular values for compact operators). | Matrix SVD is not formalized in Mathlib (only related notions like singular values for compact operators). |
modifiedEigendecomposition / diagonalization4794f8f80ac4
| Field | From #1395 | To #1841 |
|---|
| anchors | [{"section":"Decomposition","snippet":"The eigendecomposition or diagonalization expresses A as a product VDV −1"},{"type":"math_alttext","value":"{\\displaystyle {\\mathbf {A}}^{n}=({\\mathbf {VDV}}^{-1})^{n}={\\mathbf {VDV}}^{-1}{\\mathbf {VDV}}^{-1}\\ldots {\\mathbf {VDV}}^{-1}={\\mathbf {VD}}^{n}{\\mathbf {V}}^{-1}}"}] | — |
| note | Hermitian diagonalization is covered by `spectral_theorem`; general eigendecomposition is not a single statement. | Hermitian diagonalization is covered by `spectral_theorem`; general eigendecomposition is not packaged as a single statement. |
modifiedJordan decompositionb73fbd8648b2
| Field | From #1395 | To #1841 |
|---|
| anchors | [{"section":"Decomposition","snippet":"the Jordan decomposition transforms a matrix into Jordan normal form"},{"type":"math_alttext","value":"{\\displaystyle {\\mathbf {A}}^{n}=({\\mathbf {VDV}}^{-1})^{n}={\\mathbf {VDV}}^{-1}{\\mathbf {VDV}}^{-1}\\ldots {\\mathbf {VDV}}^{-1}={\\mathbf {VD}}^{n}{\\mathbf {V}}^{-1}}"}] | — |
addedMatrix exponential264595649eab
modifiedMatrix ring334d8d045c04
| Field | From #1395 | To #1841 |
|---|
| note | `Ring (Matrix n n α)` instance; isomorphism to endomorphisms is `LinearMap.toMatrixAlgEquiv`. | `Ring (Matrix n n α)` instance via `Matrix.instRing`; the endomorphism isomorphism is `LinearMap.toMatrixAlgEquiv`. |
modifiedBlock matrices6144e6679a29
| Field | From #1395 | To #1841 |
|---|
| note | `Matrix.fromBlocks` assembles a block matrix from four submatrices, with `toBlocks₁₁`/etc. extracting blocks. | `Matrix.fromBlocks` assembles a block matrix from four submatrices; `toBlocks₁₁` etc. extract blocks. |
modifiedLinear maps as matrices via bases0079e9700ddb
| Field | From #1395 | To #1841 |
|---|
| anchors | [{"section":"Relationship to linear maps","snippet":"any linear map f : V → W between finite- dimensional vector spaces can be described by a matrix"},{"type":"math_alttext","value":"{\\displaystyle f(\\mathbf {v} _{j})=\\sum _{i=1}^{m}a_{i,j}\\mathbf {w} _{i}\\qquad {\\mbox{for}}\\ j=1,\\ldots ,n.}"}] | — |
modifiedMatrix groupe559cb27cf01
| Field | From #1395 | To #1841 |
|---|
| note | Matrix groups are subgroups of `Matrix.GeneralLinearGroup`; no abstract `MatrixGroup` class. | Matrix groups appear as subgroups of `Matrix.GeneralLinearGroup`; no abstract `MatrixGroup` class. |
modifiedSpecial linear groupe039a2493c19
| Field | From #1395 | To #1841 |
|---|
| anchors | [{"section":"Matrix groups","snippet":"form a group called the special linear group of degree"},{"type":"math_alttext","value":"{\\displaystyle {\\mathbf {M}}^{\\rm {T}}{\\mathbf {M}}={\\mathbf {I}},}"}] | — |
modifiedOrthogonal groupe1dc27c9630e
| Field | From #1395 | To #1841 |
|---|
| anchors | [{"section":"Matrix groups","snippet":"The set of orthogonal matrices , determined by the condition"},{"type":"math_alttext","value":"{\\displaystyle {\\mathbf {M}}^{\\rm {T}}{\\mathbf {M}}={\\mathbf {I}},}"}] | — |
| note | `Matrix.orthogonalGroup n R := unitaryGroup n R`, satisfying `A * Aᵀ = 1`. | `Matrix.orthogonalGroup n R := unitaryGroup n R` satisfying `A * Aᵀ = 1`. |
modifiedSpecial orthogonal group98a770ede9ea
| Field | From #1395 | To #1841 |
|---|
| anchors | [{"section":"Matrix groups","snippet":"Orthogonal matrices with determinant 1 form a group called the special orthogonal group"},{"type":"math_alttext","value":"{\\displaystyle {\\mathbf {M}}^{\\rm {T}}{\\mathbf {M}}={\\mathbf {I}},}"}] | — |
modifiedEvery finite group is a matrix groupf92403960228
| Field | From #1395 | To #1841 |
|---|
| note | Cayley's theorem (finite group → permutation group) is in Mathlib, but the explicit composition with the permutation-matrix embedding into `GL n R` is not stated. | Cayley's theorem is in Mathlib, but its composition with the permutation-matrix embedding into `GL n R` is not stated. |
modifiedEmpty matrix product9766e0af1e3f
| Field | From #1395 | To #1841 |
|---|
| mathlib.decl | Matrix.mul | Matrix.mul_apply |
| note | Follows directly from `Matrix.mul_apply` with `Fintype.sum_empty`, but no dedicated lemma. | Follows directly from `Matrix.mul_apply` combined with `Fintype.sum_empty`, but no dedicated lemma packages it. |
modifiedMatrices over semiring form commutative monoid7d85eb834e62
| Field | From #1395 | To #1841 |
|---|
| note | `AddCommMonoid (Matrix m n α)` follows from `AddCommMonoid α`, which a semiring provides. | `AddCommMonoid (Matrix m n α)` follows from `AddCommMonoid α`, which a semiring provides; instance is `Matrix.addCommMonoid`. |
| provenance | ai | ai-moderated |
modifiedSquare matrices over semiring form a semiring5dc39acdda19
| Field | From #1395 | To #1841 |
|---|
| note | `instance semiring : Semiring (Matrix n n α)` for `Fintype n`, `DecidableEq n`, and `Semiring α`. | `Matrix.semiring` provides `Semiring (Matrix n n α)` under `Fintype n`, `DecidableEq n`, and `Semiring α`. |
modifiedPositive and negative determinants in a semiring7aec9ed398d2
| Field | From #1395 | To #1841 |
|---|
| note | Positive/negative determinant pair for semiring matrices is not formalized. | Positive/negative determinant pair for semiring matrices is not formalized in Mathlib. |
modifiedStochastic matrixac352da5d1ff
| Field | From #1395 | To #1841 |
|---|
| mathlib.decl | Matrix.rowStochastic | — |
| mathlib.match_kind | exact | — |
| mathlib.module | Mathlib.LinearAlgebra.Matrix.Stochastic | — |
| note | `Matrix.rowStochastic` (and `colStochastic`, `doublyStochastic`) capture stochastic matrices. | No `Matrix.rowStochastic` or `IsStochastic` declaration is in Mathlib; the underlying conditions are expressible but not packaged. |
| provenance | ai | ai-moderated |
| status | formalized | not_formalized |
modifiedRandom matricesddd97db70601
| Field | From #1395 | To #1841 |
|---|
| note | Random matrices as such are not formalized in Mathlib. | Random matrices as a named concept are not formalized in Mathlib. |
modifiedHessian matrix774808437fae
| Field | From #1395 | To #1841 |
|---|
| anchors | [{"section":"Analysis and geometry","snippet":"The Hessian matrix of a differentiable function"},{"type":"math_alttext","value":"{\\displaystyle H(f)=\\left[{\\frac {\\partial ^{2}f}{\\partial x_{i}\\,\\partial x_{j}}}\\right].}"}] | — |
modifiedLocal minimum via positive-definite Hessian1146b410b6dc
| Field | From #1395 | To #1841 |
|---|
| note | Second-derivative test for local minima via positive-definite Hessian is not in Mathlib. | The second-derivative test via positive-definite Hessian is not in Mathlib. |
modifiedJacobi matrix45d8995ab073
| Field | From #1395 | To #1841 |
|---|
| anchors | [{"section":"Analysis and geometry","snippet":"Another matrix frequently used in geometrical situations is the Jacobi matrix of a differentiable map"},{"type":"math_alttext","value":"{\\displaystyle J(f)=\\left[{\\frac {\\partial f_{i}}{\\partial x_{j}}}\\right]_{1\\leq i\\leq m,1\\leq j\\leq n}.}"}] | — |
| note | No standalone `JacobianMatrix` definition in Mathlib's analysis library; only `fderiv` (a continuous linear map). | No standalone `JacobianMatrix` in Mathlib's analysis library; only `fderiv` as a continuous linear map. |
modifiedImplicit function theorem application7fa76fd65455
| Field | From #1395 | To #1841 |
|---|
| anchors | [{"section":"Analysis and geometry","snippet":"f is locally invertible at that point, by the implicit function theorem"},{"type":"math_alttext","value":"{\\displaystyle J(f)=\\left[{\\frac {\\partial f_{i}}{\\partial x_{j}}}\\right]_{1\\leq i\\leq m,1\\leq j\\leq n}.}"}] | — |