Matrix.isUnit_det_of_left_inverse
theorem Matrix.isUnit_det_of_left_inverse :
∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] {A B : Matrix n n α},
B * A = 1 → IsUnit A.det
This theorem states that for any finite type `n` and any type `α` that forms a commutative ring, given two matrices `A` and `B` of type `Matrix n n α`, if the multiplication of `B` and `A` results in an identity matrix, then the determinant of matrix `A` is a unit in the ring `α`. Here, a unit in the ring is an element which has a multiplicative inverse.
More concisely: If matrices `A` and `B` of size `n x n` over a commutative ring `α` satisfy `B * A = id_α`, then the determinant of `A` is a unit in `α`.
|
Matrix.nonsing_inv_nonsing_inv
theorem Matrix.nonsing_inv_nonsing_inv :
∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α),
IsUnit A.det → A⁻¹⁻¹ = A
This theorem, `Matrix.nonsing_inv_nonsing_inv`, states that for any finite type `n`, any type `α` that forms a commutative ring, and any matrix `A` of type `Matrix n n α`, if the determinant of `A` is a unit (i.e., it has a multiplicative inverse, which means the matrix `A` is invertible), then the double inverse of `A` (i.e., `(A⁻¹)⁻¹`) is equal to `A` itself. This theorem essentially asserts the fundamental property of invertible matrices in a generalised algebraic setting.
More concisely: If a square matrix over a commutative ring with unit determinant is invertible, then its double inverse is equal to the original matrix.
|
Matrix.invOf_eq_nonsing_inv
theorem Matrix.invOf_eq_nonsing_inv :
∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α)
[inst_3 : Invertible A], ⅟A = A⁻¹
The theorem `Matrix.invOf_eq_nonsing_inv` states that for any type `n` with a finite number of elements (`Fintype n`) and decidable equality (`DecidableEq n`), and any commutative ring `α`, for any `n` by `n` matrix `A` with elements from `α` that is invertible (`Invertible A`), the multiplicative inverse of `A` (`⅟A`) is equal to its nonsingular inverse (`A⁻¹`). In simpler terms, this theorem asserts that for a square matrix `A` from a commutative ring which is invertible, its multiplicative inverse and nonsingular inverse are the same.
More concisely: For any commutative ring α, finite type n with decidable equality, and invertible n by n matrix A over α, the multiplicative inverse and nonsingular inverse of A are equal.
|
Matrix.nonsing_inv_mul
theorem Matrix.nonsing_inv_mul :
∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α),
IsUnit A.det → A⁻¹ * A = 1
The theorem `Matrix.nonsing_inv_mul` states that for any square matrix `A` of type `Matrix n n α`, where `n` is a finite type with decidable equality, and `α` is a commutative ring, if the determinant of `A` is a unit (i.e., it has a multiplicative inverse), then the non-singular inverse of `A` is its left inverse. In other words, when multiplied from the left by its inverse, `A` yields the identity matrix. This is written mathematically as `A⁻¹ * A = 1`.
More concisely: If a square matrix `A` of type `Matrix n n α` over a commutative ring `α` with decidable equality and non-zero determinant has an inverse, then `A` and its inverse are multiplicative inverses, i.e., `A * A⁻¹ = 1`.
|
Matrix.det_conj'
theorem Matrix.det_conj' :
∀ {m : Type u} {α : Type v} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : CommRing α] {M : Matrix m m α},
IsUnit M → ∀ (N : Matrix m m α), (M⁻¹ * N * M).det = N.det
The theorem `Matrix.det_conj'` asserts that for any type `m` with a finite number of elements and decidable equality, a type `α` which forms a commutative ring, a matrix `M` with entries from `α` and indices from `m`, if `M` is a unit (i.e., it has a two-sided inverse), then for any matrix `N` of the same type as `M`, the determinant of the matrix resulting from the multiplication of the inverse of `M`, `N`, and `M` in that order, is equal to the determinant of `N`. In mathematical terms, this corresponds to the statement that if `M` is invertible, then det(`M⁻¹NM`) = det(`N`).
More concisely: If `M` is an invertible matrix with entries from a commutative ring of finite type with decidable equality, then det(`M⁻¹NM`) = det(`N`).
|
Matrix.det_smul_inv_vecMul_eq_cramer_transpose
theorem Matrix.det_smul_inv_vecMul_eq_cramer_transpose :
∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α)
(b : n → α), IsUnit A.det → A.det • Matrix.vecMul b A⁻¹ = A.transpose.cramer b
This theorem is a form of Cramer's rule in linear algebra. For any finite type `n`, type `α` with a commutative ring structure, a matrix `A` of type `α` with indices from `n` and a vector `b` of type `α` with indices from `n`, if the determinant of `A` is a unit (i.e., it has a multiplicative inverse), then the scalar product of `A`'s determinant and the matrix-vector multiplication of `b` and the inverse of `A` is equal to the result of applying the Cramer's rule on the transpose of `A` with `b`. Cramer's rule is a method for solving system of linear equations by expressing the solution in terms of determinants.
More concisely: For a square matrix `A` of determinant `d` over a commutative ring `α` with a unit `d`, the solution `x` to the system `Ax = b` given by Cramer's rule is equivalent to `d * (A⁺T * b)`, where `A⁺` is the matrix inverse of `A` and `T` denotes the transpose.
|
Mathlib.LinearAlgebra.Matrix.NonsingularInverse._auxLemma.4
theorem Mathlib.LinearAlgebra.Matrix.NonsingularInverse._auxLemma.4 :
∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α)
[inst_3 : Invertible A], A⁻¹ = ⅟A
The theorem `Mathlib.LinearAlgebra.Matrix.NonsingularInverse._auxLemma.4` states that for any types `l`, `m`, `n`, `o`, and `α`, where `α` is a non-unital semiring, and `m` and `n` are finite types, given any matrices `L` of type `Matrix l m α`, `M` of type `Matrix m n α` and `N` of type `Matrix n o α`, the multiplication operation on matrices is associative. In other words, the product of `L` and the product of `M` and `N` is the same as the product of the product of `L` and `M` and `N` - formally, `L * (M * N)` equals `L * M * N`.
More concisely: For matrices $L$ of size $m \times l$, $M$ of size $l \times n$, and $N$ of size $n \times o$ over a non-unital semiring $\alpha$, the associativity of matrix multiplication holds: $L *(M * N) = (L * M) * N$.
|
Matrix.conjTranspose_nonsing_inv
theorem Matrix.conjTranspose_nonsing_inv :
∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α)
[inst_3 : StarRing α], A⁻¹.conjTranspose = A.conjTranspose⁻¹
This theorem states that for any type `n` that has a finite number of elements and decidable equality, and any `α` that forms a commutative ring with a star operation, the conjugate transpose of the inverse of a square matrix `A` with elements from `α` and indices from `n` is equal to the inverse of the conjugate transpose of `A`. In simpler terms, it says that the conjugate transpose operation commutes with inversion for any square matrix in a star commutative ring.
More concisely: For any square matrix `A` with coefficients in a commutative ring `α` with a star operation and finite index set `n` of decidable equality, the conjugate transpose of `A`'s inverse is equal to the inverse of `A`'s conjugate transpose.
|
Matrix.right_inv_eq_left_inv
theorem Matrix.right_inv_eq_left_inv :
∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α]
{A B C : Matrix n n α}, A * B = 1 → C * A = 1 → B = C
This theorem states that for any type `n` (which is a `Fintype`, i.e., a finite set), and for any type `α` (which operates under the rules of a `CommRing`, i.e., a commutative ring), if `A`, `B`, and `C` are square matrices (matrices of size `n x n` with entries from `α`), then if `A * B` equals the identity matrix and `C * A` also equals the identity matrix, then `B` is equal to `C`. In other words, the right inverse of a matrix `A` is the same as the left inverse of `A`, when they both exist.
More concisely: If `A` is a square `n x n` matrix over a commutative ring `α` such that `A * B = I` and `C * A = I` for some matrices `B` and `C` of size `n x n` with entries from `α`, then `B = C`.
|
Matrix.mul_nonsing_inv
theorem Matrix.mul_nonsing_inv :
∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α),
IsUnit A.det → A * A⁻¹ = 1
This theorem states that for any square matrix `A` of type `Matrix n n α`, where `n` is a finite type with decidable equality, and `α` is a commutative ring, if the determinant of `A` is a unit (i.e., it has a multiplicative inverse), then the product of `A` and its nonsingular inverse `A⁻¹` equals the identity matrix. In other words, if the determinant of `A` is not zero (which indicates that `A` is nonsingular), then `A⁻¹` is a right inverse of `A`.
More concisely: If `A` is a square matrix of type `n x n` over a commutative ring `α` with a nonzero determinant, then `A` and its inverse `A⁻¹` are multiplicative inverses: `A * A⁻¹ = id`.
|
Matrix.vecMul_injective_iff_isUnit
theorem Matrix.vecMul_injective_iff_isUnit :
∀ {m : Type u} [inst : DecidableEq m] {K : Type u_3} [inst_1 : Field K] [inst_2 : Fintype m] {A : Matrix m m K},
(Function.Injective fun v => Matrix.vecMul v A) ↔ IsUnit A
This theorem states that for any type `m` with decidable equality, any field `K`, and any finite type `m`, a matrix `A` of type `Matrix m m K` is such that the function which multiplies a vector `v` with `A` is injective if and only if `A` is a unit in the monoid of matrices. In other words, the function that multiplies a vector `v` by `A` is injective (meaning no two distinct vectors produce the same result when multiplied by `A`) if and only if `A` has an inverse in the multiplication of matrices (i.e., `A` is a unit in the monoid of matrices).
More concisely: For any decidably equal type `m`, field `K`, and finite `m`-by-`m` matrix `A` over `K`, the multiplication function `x ↦ Ax` is injective if and only if `A` has an inverse in the monoid of `m`-by-`m` matrices over `K`.
|
Matrix.right_inv_eq_right_inv
theorem Matrix.right_inv_eq_right_inv :
∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α]
{A B C : Matrix n n α}, A * B = 1 → A * C = 1 → B = C
This theorem states that for any types `n` and `α`, where `n` is a finite type with decidable equality and `α` is a commutative ring, given three matrices `A`, `B`, and `C` with entries in `α`, if `B` is a right inverse of `A` (i.e., `A * B = 1`, where `1` is the identity matrix) and `C` is also a right inverse of `A` (i.e., `A * C = 1`), then `B` and `C` must be the same matrix (i.e., `B = C`). In other words, the right inverse of a matrix, when it exists, is unique.
More concisely: If `A` is a finite type with decidable equality and `α` is a commutative ring, then any two right inverses of `A` in the matrix multiplication over `α` are equal.
|
Matrix.nonsing_inv_eq_ring_inverse
theorem Matrix.nonsing_inv_eq_ring_inverse :
∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α),
A⁻¹ = Ring.inverse A
This theorem states that for any square matrix `A` over a commutative ring `α`, where the size of the matrix is a finite type `n` with a decidable equality, the nonsingular inverse of `A` is identical to the general `Ring.inverse` of `A`. Essentially, if `A` is invertible in the matrix sense, then its matrix inverse is the same as the ring-theoretic multiplicative inverse.
More concisely: For any square matrix `A` over a commutative ring `α` of finite type `n` with decidable equality, if `A` has an inverse in the matrix sense, then `A`'s matrix inverse is equal to its ring-theoretic multiplicative inverse.
|
Matrix.inv_eq_left_inv
theorem Matrix.inv_eq_left_inv :
∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] {A B : Matrix n n α},
B * A = 1 → A⁻¹ = B
This theorem states that for any type `n` that is a finite type with decidable equality and any commutative ring `α`, if a matrix `A` of type `Matrix n n α` (a matrix with entries in `α` and both rows and columns indexed by `n`) has a left inverse `B` (i.e., `B * A` equals the identity matrix), then the inverse of `A` is equal to `B`. In more mathematical terms, if $BA = I$ for matrices $A$ and $B$ over a commutative ring, then $A^{-1} = B$.
More concisely: If `A` is a finite type with decidable equality and `α` is a commutative ring such that `A` has a left inverse `B` over `α`, then `B` is the right inverse (and hence the inverse) of `A`.
|
Matrix.det_smul_inv_mulVec_eq_cramer
theorem Matrix.det_smul_inv_mulVec_eq_cramer :
∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α)
(b : n → α), IsUnit A.det → A.det • A⁻¹.mulVec b = A.cramer b
This theorem is one form of Cramer's rule. It states that for any given type `n` with a finite number of elements and decidable equality, and any commutative ring `α`, if we have a matrix `A` of type `n x n` with elements from `α` and a vector `b` of type `n` with elements from `α`, and the determinant of `A` is a unit (i.e., has a multiplicative inverse), then the determinant of `A` scaled by the product of the inverse of `A` and `b` is equal to the Cramer's rule result of `A` and `b`. In mathematical notation, if `det(A)` is a unit, then `det(A) * (A⁻¹ * b) = A.cramer(b)`.
More concisely: If matrix `A` of size `n x n` over commutative ring `α` with a finite number of elements and decidable equality has a unit determinant, then `det(A) * (A⁻¹ * b) = A.cramer b`, where `b` is a vector of size `n` over `α` and `A.cramer b` is the vector obtained by applying Cramer's rule to `A` and `b`.
|
Matrix.det_conj
theorem Matrix.det_conj :
∀ {m : Type u} {α : Type v} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : CommRing α] {M : Matrix m m α},
IsUnit M → ∀ (N : Matrix m m α), (M * N * M⁻¹).det = N.det
The theorem `Matrix.det_conj` states that for a square matrix `M` over a commutative ring `α`, if `M` is a unit (i.e., it has a two-sided inverse), then for any square matrix `N` over the same commutative ring, the determinant of the matrix obtained by conjugating `N` with `M` (i.e., the product of `M`, `N`, and the inverse of `M`) is equal to the determinant of `N`. This is essentially an assertion of the invariance of the determinant under conjugation by an invertible matrix.
More concisely: If `M` is a unit in a commutative ring `α` and `N` is any square matrix over `α`, then the determinant of `MNM⁻¹` is equal to the determinant of `N`.
|
Matrix.nonsing_inv_apply_not_isUnit
theorem Matrix.nonsing_inv_apply_not_isUnit :
∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α),
¬IsUnit A.det → A⁻¹ = 0
This theorem states that for any square matrix `A` of type `α` with indices of type `n`, if the determinant of `A` is not a unit in the commutative ring `α`, then the inverse of `A` is the zero matrix. In other words, if the determinant of the matrix is not invertible (i.e., the matrix is singular), then the matrix does not have an inverse in the usual sense, and this is represented in Lean by the inverse equalling the zero matrix. This is a fundamental result in linear algebra.
More concisely: If the determinant of a square matrix over a commutative ring is not a unit, then the matrix has no multiplicative inverse and is equal to its own inverse (zero matrix).
|
Matrix.coe_units_inv
theorem Matrix.coe_units_inv :
∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α]
(A : (Matrix n n α)ˣ), ↑A⁻¹ = (↑A)⁻¹
The theorem `Matrix.coe_units_inv` states that for any type `n` which is a `Fintype` and has `DecidableEq`, and any commutative ring `α`, if `A` is an invertible (nonsingular) matrix with entries in `α` and indexes in `n`, then the inverse of `A` when treated as an ordinary matrix (coerced from the unit group of matrices) is the same as the matrix inverse of `A`. This theorem connects the concept of inverse in the group of units with the concept of matrix inverse.
More concisely: For any commutative ring `α`, if `A` is an invertible matrix over `α` with entries indexed by a `Fintype` with `DecidableEq`, then the coerced unit inverse of `A` equals its matrix inverse.
|
Matrix.inv_eq_right_inv
theorem Matrix.inv_eq_right_inv :
∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] {A B : Matrix n n α},
A * B = 1 → A⁻¹ = B
This theorem states that for any type `n` representing the indices of a matrix and any type `α` representing a commutative ring (the set of values of the matrix entries), if we have a matrix `A` and another matrix `B` such that the product of `A` and `B` equals the identity matrix, then the inverse matrix of `A` is equal to `B`. The conditions require that `n` is finite and has decidable equality, and the entries of the matrix belong to a commutative ring.
More concisely: If matrices `A` and `B` of finite, decidably equal indices over a commutative ring have the product `AB` equal to the identity matrix, then `B` is the inverse of `A`.
|
Matrix.mul_inv_rev
theorem Matrix.mul_inv_rev :
∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A B : Matrix n n α),
(A * B)⁻¹ = B⁻¹ * A⁻¹
This theorem states that for any type `n` and a type `α` with a commutative ring structure, given any finite type `n` (with decidable equality) and any two square matrices `A` and `B` with entries in `α`, the inverse of the product of `A` and `B` is equal to the product of the inverse of `B` and the inverse of `A`, in that order. This is essentially stating the rule of reversing the order of multiplication when taking the inverse of a product of two elements, but for matrices. In mathematical terms, given two matrices $(A,B)$, we have $(AB)^{-1} = B^{-1}A^{-1}$.
More concisely: For any commutative ring `α` and finite type `n` with decidable equality, if `A` and `B` are square matrices of size `n x n` over `α` with inverses, then `A⁻¹ * B⁻¹ = B⁻¹ * A⁻¹`.
|
Matrix.invOf_eq
theorem Matrix.invOf_eq :
∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α)
[inst_3 : Invertible A.det] [inst_4 : Invertible A], ⅟A = ⅟A.det • A.adjugate
This theorem states that for any type `n` representing the indices of rows and columns, and any type `α` representing the entries of a matrix, given that `n` is finite (`Fintype n`), equality on `n` is decidable (`DecidableEq n`), and `α` forms a commutative ring (`CommRing α`), if a matrix `A` of dimensions `n x n` with entries in `α` has an invertible determinant (`Invertible (Matrix.det A)`) and the matrix `A` itself is invertible (`Invertible A`), then the multiplicative inverse of the matrix `A` (represented as `⅟A`) is equal to the multiplicative inverse of the determinant of `A` (represented as `⅟(Matrix.det A)`) scaled by the adjugate of `A` (`Matrix.adjugate A`). In mathematical notation, this theorem states that $A^{-1} = \frac{1}{det(A)} \cdot adj(A)$, where $adj(A)$ is the adjugate matrix of $A$.
More concisely: If `n` is a finite type, `α` is a commutative ring, `A` is an `n x n` matrix over `α` with invertible determinant and inverse, then `A^(-1) = 1 / det(A) * adj(A)`.
|
Matrix.isUnit_iff_isUnit_det
theorem Matrix.isUnit_iff_isUnit_det :
∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α),
IsUnit A ↔ IsUnit A.det
This theorem states that for any square matrix `A` of a certain type `α` with its rows and columns indexed by a finite type `n`, the matrix `A` is a unit (i.e., it has a two-sided inverse) if and only if the determinant of `A` is a unit. This is within a context where `n` is a finite type, `α` has a commutative ring structure, and equality of `n` elements is decidable. In other words, a matrix is invertible if and only if its determinant is non-zero and hence invertible in the commutative ring `α`.
More concisely: A square matrix of finite type `n` over a commutative ring `α` with decidable equality is invertible if and only if its determinant is a non-zero unit in `α`.
|
Matrix.isUnit_submatrix_equiv
theorem Matrix.isUnit_submatrix_equiv :
∀ {m : Type u} {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α]
[inst_3 : Fintype m] [inst_4 : DecidableEq m] {A : Matrix m m α} (e₁ e₂ : n ≃ m),
IsUnit (A.submatrix ⇑e₁ ⇑e₂) ↔ IsUnit A
This theorem states that for any types `m`, `n`, and `α`, given that `n` and `m` are finite types, `n` and `m` have decidable equality, and `α` is a commutative ring, for any matrix `A` of type `Matrix m m α` and any two equivalences `e₁` and `e₂` from `n` to `m`, the submatrix of `A` (indexed by `e₁` and `e₂`) is a unit (i.e., has a two-sided inverse) if and only if `A` itself is a unit. This is important in the context of linear algebra, as it establishes a correspondence between the invertibility of a matrix and its submatrix.
More concisely: For any commutative ring `α`, finite types `m` and `n`, and matrices `A` of size `m x m` over `α`, if `A` is a unit and `e₁` and `e₂` are equivalences from `n` to `m`, then the submatrix of `A` indexed by `e₁` and `e₂` is also a unit.
|
Matrix.left_inv_eq_left_inv
theorem Matrix.left_inv_eq_left_inv :
∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α]
{A B C : Matrix n n α}, B * A = 1 → C * A = 1 → B = C
This theorem states that for any given type `n` and a type `α` defined over a commutative ring, if we have three matrices `A`, `B` and `C` (all of type `Matrix n n α`), then if `B` and `C` are both left inverses of `A` (meaning that the product of `B` and `A`, as well as the product of `C` and `A`, both equal the identity matrix), then `B` and `C` must be equal to each other. This essentially implies that the left inverse of a matrix, when it exists, is unique.
More concisely: If two matrices of size `n x n` over a commutative ring are both left inverses of the same matrix, then they are equal.
|
Matrix.mul_nonsing_inv_cancel_left
theorem Matrix.mul_nonsing_inv_cancel_left :
∀ {m : Type u} {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α]
(A : Matrix n n α) (B : Matrix n m α), IsUnit A.det → A * (A⁻¹ * B) = B
This theorem states that for any two matrices `A` and `B` of types `Matrix n n α` and `Matrix n m α` respectively, where `n` is any finite type with decidable equality and `α` is a commutative ring, if the determinant of matrix `A` is a unit in the ring `α` (i.e., it has a multiplicative inverse), then multiplying `A` with the result of multiplying the inverse of `A` with `B` gives us back matrix `B`. In other words, if `A` is invertible (its determinant is non-zero), then the equation `A * (A⁻¹ * B) = B` holds. This is a mathematical formulation of the property of matrix multiplication that the product of a matrix and its inverse is always the identity matrix, hence cancelling each other out.
More concisely: If `A` is an invertible `n x n` matrix over a commutative ring `α`, then `A * (A⁻¹ * B) = B` for any `n x m` matrix `B` over `α`.
|
Matrix.isUnit_diagonal
theorem Matrix.isUnit_diagonal :
∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] {v : n → α},
IsUnit (Matrix.diagonal v) ↔ IsUnit v
This theorem, `Matrix.isUnit_diagonal`, states that for any type `n` with a finite number of elements (`Fintype n`), type `α` that forms a commutative ring (`CommRing α`), and a function `v : n → α`, the square matrix derived from `v` using the `Matrix.diagonal` function is a unit in the monoid of matrices if and only if `v` is a unit in the monoid of `α`. Here, a "unit" means an element with a two-sided inverse. The equivalence is established in both directions, meaning that if `v` is a unit, then the diagonal matrix derived from `v` is also a unit, and vice versa.
More concisely: For any commutative ring `α` with a finite number of elements `n` and a unit `v : n → α`, the diagonal matrix derived from `v` using `Matrix.diagonal` is a unit in the monoid of matrices if and only if `v` is a unit in `α`.
|
Matrix.list_prod_inv_reverse
theorem Matrix.list_prod_inv_reverse :
∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α]
(l : List (Matrix n n α)), l.prod⁻¹ = (List.map Inv.inv l.reverse).prod
This theorem, `Matrix.list_prod_inv_reverse`, states that for any finite type `n`, any type `α` that forms a commutative ring, and a list `l` of matrices with entries in `α` and row/column indices in `n`, the inverse of the product of all matrices in the list is equal to the product of the inverses of all matrices in the reversed list. In other words, if you take a list of matrices, multiply them all together and take the inverse, it's the same as if you reversed the list, took the inverse of each matrix individually, and then multiplied them all together. This theorem relies on the ability to decide equality in `n`, the fact that `α` forms a commutative ring, and the finiteness of `n`.
More concisely: For any finite type `n`, commutative ring `α`, and list `l` of `n x n` matrices `M` over `α`, the inverse of the product of all matrices in `l` is equal to the product of the inverses of all matrices in the reversed list `l.reverse`.
|
Matrix.mul_eq_one_comm
theorem Matrix.mul_eq_one_comm :
∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] {A B : Matrix n n α},
A * B = 1 ↔ B * A = 1
This theorem states that, for any type `n`, type `α`, where `n` is a finite type, `n` has decidable equality, and `α` is a commutative ring, if `A` and `B` are square matrices with entries in `α` and dimensions indexed by `n`, then the product of `A` and `B` equals the identity matrix if and only if the product of `B` and `A` equals the identity matrix. In other words, `A` and `B` are inverses with respect to matrix multiplication in either order.
More concisely: For any finite type `n` and commutative ring `α`, if `n` has decidable equality and square matrices `A` and `B` of dimension `n` over `α` have equal products with the identity matrix in either order, then `A` and `B` are inverses of each other with respect to matrix multiplication.
|
Matrix.isUnit_det_of_invertible
theorem Matrix.isUnit_det_of_invertible :
∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α)
[inst_3 : Invertible A], IsUnit A.det
This theorem states that for any square matrix `A` with indices of type `n` and elements of type `α`, where `α` is a type over a commutative ring, and `n` is a finite type with decidable equality, if `A` is invertible, then the determinant of `A` is a unit in the commutative ring `α`. In terms of linear algebra, this essentially means that the determinant of any invertible square matrix is a non-zero element in the underlying field or ring, thus having a multiplicative inverse.
More concisely: If `A` is a square matrix of type `n x n` over a commutative ring `α` with decidable equality and `n` finite, and `A` is invertible, then the determinant of `A` is a unit in `α`.
|
Matrix.inv_def
theorem Matrix.inv_def :
∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α),
A⁻¹ = Ring.inverse A.det • A.adjugate
This theorem, `Matrix.inv_def`, defines the inverse of a matrix. More precisely, it states that for any matrix `A` indexed by a finite type `n` with coefficients in a commutative ring `α`, the inverse of `A` is equal to the scalar product of the ring inverse of the determinant of `A` and the adjugate of `A`. In mathematical notation, this would be written as `A⁻¹ = (det(A))⁻¹ * adjugate(A)`. Here `•` denotes scalar multiplication, `Ring.inverse` the ring inverse (or reciprocal) function which sends `x` to `x⁻¹` if `x` is invertible and to `0` otherwise, and `Matrix.det` and `Matrix.adjugate` are the determinant and adjugate of the matrix respectively.
More concisely: For a matrix `A` of size `n x n` over a commutative ring `α`, its inverse is equal to the product of the ring inverse of its determinant and its adjugate: `A⁻¹ = (det(A))⁻¹ * adjugate(A)`.
|