Documentation

Mathlib.LinearAlgebra.Matrix.Nondegenerate

Matrices associated with non-degenerate bilinear forms #

Main definitions #

def Matrix.Nondegenerate {m : Type u_1} {R : Type u_2} [Fintype m] [CommRing R] (M : Matrix m m R) :

A matrix M is nondegenerate if for all v ≠ 0, there is a w ≠ 0 with w * M * v ≠ 0.

Equations
Instances For
    theorem Matrix.Nondegenerate.eq_zero_of_ortho {m : Type u_1} {R : Type u_2} [Fintype m] [CommRing R] {M : Matrix m m R} (hM : Matrix.Nondegenerate M) {v : mR} (hv : ∀ (w : mR), Matrix.dotProduct v (Matrix.mulVec M w) = 0) :
    v = 0

    If M is nondegenerate and w * M * v = 0 for all w, then v = 0.

    theorem Matrix.Nondegenerate.exists_not_ortho_of_ne_zero {m : Type u_1} {R : Type u_2} [Fintype m] [CommRing R] {M : Matrix m m R} (hM : Matrix.Nondegenerate M) {v : mR} (hv : v 0) :

    If M is nondegenerate and v ≠ 0, then there is some w such that w * M * v ≠ 0.

    theorem Matrix.nondegenerate_of_det_ne_zero {m : Type u_1} {A : Type u_3} [Fintype m] [CommRing A] [IsDomain A] [DecidableEq m] {M : Matrix m m A} (hM : Matrix.det M 0) :

    If M has a nonzero determinant, then M as a bilinear form on n → A is nondegenerate.

    See also BilinForm.nondegenerateOfDetNeZero' and BilinForm.nondegenerateOfDetNeZero.

    theorem Matrix.eq_zero_of_vecMul_eq_zero {m : Type u_1} {A : Type u_3} [Fintype m] [CommRing A] [IsDomain A] [DecidableEq m] {M : Matrix m m A} (hM : Matrix.det M 0) {v : mA} (hv : Matrix.vecMul v M = 0) :
    v = 0
    theorem Matrix.eq_zero_of_mulVec_eq_zero {m : Type u_1} {A : Type u_3} [Fintype m] [CommRing A] [IsDomain A] [DecidableEq m] {M : Matrix m m A} (hM : Matrix.det M 0) {v : mA} (hv : Matrix.mulVec M v = 0) :
    v = 0