Matrix.det_ne_zero_of_sum_col_pos
theorem Matrix.det_ne_zero_of_sum_col_pos :
∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {S : Type u_2} [inst_2 : LinearOrderedCommRing S]
{A : Matrix n n S},
(Pairwise fun i j => A i j < 0) → (∀ (j : n), 0 < Finset.univ.sum fun i => A i j) → A.det ≠ 0
This theorem states that for any square matrix `A` of order `n` with entries in a linearly ordered commutative ring `S`, if all off-diagonal entries of `A` are negative and the sum of the entries of each column is positive, then the determinant of `A` is not zero. In other words, such a matrix is invertible. The type `n` is assumed to be finite and equipped with a decidable equality relation.
More concisely: If `A` is a square matrix of order `n` over a linearly ordered commutative ring `S` with finite `n` and decidable equality, having all off-diagonal entries negative and each column sum positive, then the determinant of `A` is non-zero.
|
Matrix.Nondegenerate.det_ne_zero
theorem Matrix.Nondegenerate.det_ne_zero :
∀ {n : Type u_1} [inst : Fintype n] {A : Type u_4} [inst_1 : DecidableEq n] [inst_2 : CommRing A]
[inst_3 : IsDomain A] {M : Matrix n n A}, M.Nondegenerate → M.det ≠ 0
This theorem states that for any type `n` being a finite type, any type `A` being a commutative ring and also a domain, and any `n x n` matrix `M` with entries in `A`, if the matrix `M` is non-degenerate (i.e., it does not map distinct vectors to the same vector), then the determinant of the matrix `M` is not equal to zero. The `DecidableEq n` instance implies that equality between elements of type `n` is decidable.
More concisely: If `M` is an `n x n` non-degenerate matrix over a commutative domain `A` in Lean 4, then the determinant of `M` is non-zero.
|
Matrix.nondegenerate_iff_det_ne_zero
theorem Matrix.nondegenerate_iff_det_ne_zero :
∀ {n : Type u_1} [inst : Fintype n] {A : Type u_4} [inst_1 : DecidableEq n] [inst_2 : CommRing A]
[inst_3 : IsDomain A] {M : Matrix n n A}, M.Nondegenerate ↔ M.det ≠ 0
The theorem `Matrix.nondegenerate_iff_det_ne_zero` states that for any finite type `n`, any type `A` with a decidable equality, a commutative ring structure, and a domain structure, and any matrix `M` with entries in `A` and indices in `n`, the matrix `M` is nondegenerate if and only if the determinant of `M` is not equal to zero. In the context of this theorem, a matrix `M` is defined as nondegenerate if for all vectors `v` not equal to the zero vector, there exists a vector `w` not equal to the zero vector such that the dot product of `v` and `M` multiplied by `w` is not equal to zero.
More concisely: A square matrix over a commutative ring with unity and a decidable equality is nondegenerate if and only if its determinant is nonzero.
|
Matrix.det_ne_zero_of_sum_row_pos
theorem Matrix.det_ne_zero_of_sum_row_pos :
∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {S : Type u_2} [inst_2 : LinearOrderedCommRing S]
{A : Matrix n n S},
(Pairwise fun i j => A i j < 0) → (∀ (i : n), 0 < Finset.univ.sum fun j => A i j) → A.det ≠ 0
The theorem `Matrix.det_ne_zero_of_sum_row_pos` states that for any square matrix `A` over a linearly ordered commutative ring `S`, if every off-diagonal entry of `A` is negative and the sum of the entries in each row of `A` is positive, then the determinant of `A` is not zero. Here, the row and column indices of the matrix `A` are drawn from some finite set `n` for which equality is decidable.
In other words, this theorem proves that a matrix, whose entries outside the main diagonal are all negative and where each row sums up to a positive number, has a non-zero determinant.
More concisely: If `A` is a square matrix over a linearly ordered commutative ring with every off-diagonal entry negative and each row having a positive sum, then the determinant of `A` is non-zero.
|
Matrix.exists_mulVec_eq_zero_iff_aux
theorem Matrix.exists_mulVec_eq_zero_iff_aux :
∀ {n : Type u_1} [inst : Fintype n] {K : Type u_4} [inst_1 : DecidableEq n] [inst_2 : Field K] {M : Matrix n n K},
(∃ v, v ≠ 0 ∧ M.mulVec v = 0) ↔ M.det = 0
This theorem, `Matrix.exists_mulVec_eq_zero_iff_aux`, states that for any finite type `n`, any type `K` that is a field, and any `n x n` matrix `M` with elements from `K`, the existence of a non-zero vector `v` such that when it is multiplied by `M`, the result is the zero vector, is equivalent to the determinant of `M` being zero. In other words, a matrix has a determinant of zero if and only if there is a non-zero vector that becomes the zero vector when multiplied by the matrix. This theorem is applicable for all integral domains but here it is proved first for the field of fractions for simplicity.
More concisely: A square matrix over a field has a determinant of zero if and only if there exists a non-zero vector that it maps to the zero vector upon multiplication.
|
Matrix.Nondegenerate.of_det_ne_zero
theorem Matrix.Nondegenerate.of_det_ne_zero :
∀ {n : Type u_1} [inst : Fintype n] {A : Type u_4} [inst_1 : DecidableEq n] [inst_2 : CommRing A]
[inst_3 : IsDomain A] {M : Matrix n n A}, M.det ≠ 0 → M.Nondegenerate
This theorem, named `Matrix.Nondegenerate.of_det_ne_zero`, states that for any finite type `n`, any type `A` that has decidable equality and is a commutative ring and is also a domain, and any `n x n` matrix `M` with entries in `A`, if the determinant of `M` is not equal to zero, then the matrix `M` is nondegenerate.
In more mathematical terms, this theorem asserts that if a square matrix has a non-zero determinant, then the matrix is nondegenerate, meaning that it has full rank. This is a key property in linear algebra as it implies that the matrix is invertible.
More concisely: If `M` is an `n x n` matrix over a commutative ring `A` that is a domain and has decidable equality, then `M` is nondegenerate (has full rank) whenever its determinant is non-zero.
|