Matrix.Nondegenerate.exists_not_ortho_of_ne_zero
theorem Matrix.Nondegenerate.exists_not_ortho_of_ne_zero :
∀ {m : Type u_1} {R : Type u_2} [inst : Fintype m] [inst_1 : CommRing R] {M : Matrix m m R},
M.Nondegenerate → ∀ {v : m → R}, v ≠ 0 → ∃ w, Matrix.dotProduct v (M.mulVec w) ≠ 0
The theorem `Matrix.Nondegenerate.exists_not_ortho_of_ne_zero` states that for any finite type `m` and any commutative ring `R`, if we have a nondegenerate matrix `M` with entries in `R` and indexed by `m`, and if we have a non-zero vector `v` with entries in `R` and indexed by `m`, then there exists another vector `w` such that the dot product of `v` and the result of multiplying `M` by `w` is non-zero. Essentially, this means that if a matrix is nondegenerate (its determinant isn't zero), then for any non-zero vector, we can find another vector such that their matrix multiplication yields a non-zero result.
More concisely: For any nondegenerate matrix `M` of size `m` over a commutative ring `R` and any non-zero vector `v` of length `m` over `R`, there exists a vector `w` such that `v · M · w ≠ 0`.
|
Matrix.Nondegenerate.eq_zero_of_ortho
theorem Matrix.Nondegenerate.eq_zero_of_ortho :
∀ {m : Type u_1} {R : Type u_2} [inst : Fintype m] [inst_1 : CommRing R] {M : Matrix m m R},
M.Nondegenerate → ∀ {v : m → R}, (∀ (w : m → R), Matrix.dotProduct v (M.mulVec w) = 0) → v = 0
The theorem `Matrix.Nondegenerate.eq_zero_of_ortho` states that for a given nondegenerate matrix `M` with entries in a commutative ring `R` and indexed by `m`, if for every vector `w`, the dot product of vector `v` and the matrix-vector product of `M` and `w` equals zero, then the vector `v` must be the zero vector. In other words, if `M` is nondegenerate and the dot product of `v` and `Mw` is zero for all `w`, then `v` must be zero. This theorem is crucial in linear algebra, as it provides a condition under which a vector must be the zero vector in the context of nondegenerate matrices.
More concisely: If a nondegenerate matrix times any vector results in the zero vector for the dot product, then the original vector is the zero vector.
|
Matrix.nondegenerate_of_det_ne_zero
theorem Matrix.nondegenerate_of_det_ne_zero :
∀ {m : Type u_1} {A : Type u_3} [inst : Fintype m] [inst_1 : CommRing A] [inst_2 : IsDomain A]
[inst_3 : DecidableEq m] {M : Matrix m m A}, M.det ≠ 0 → M.Nondegenerate
The theorem `Matrix.nondegenerate_of_det_ne_zero` states that for any type `m` with finite elements, and any commutative ring `A` which is also an integral domain, if a square matrix `M` with dimensions indexed by `m` and elements from `A` has a determinant that is not zero, then `M` is a nondegenerate bilinear form when applied to the function `n → A`. This essentially means that `M` has full rank or, in other words, the columns of `M` are linearly independent. Note that the equality of elements of `m` is decidable.
The theorem also refers to other related theorems, `BilinForm.nondegenerateOfDetNeZero'` and `BilinForm.nondegenerateOfDetNeZero`, for more information on nondegenerate bilinear forms.
More concisely: For any square matrix `M` of finite type `m` over a commutative ring `A` that is an integral domain with non-zero determinant, `M` represents a nondegenerate bilinear form.
|