Matrices associated with non-degenerate bilinear forms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main definitions #

matrix.nondegenerate A: the proposition that when interpreted as a bilinear form, the matrix A is nondegenerate.

def matrix.nondegenerate {m : Type u_1} {R : Type u_2} [fintype m] [comm_ring R] (M : matrix m m R) :

Prop

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

Equations

theorem matrix.nondegenerate.eq_zero_of_ortho {m : Type u_1} {R : Type u_2} [fintype m] [comm_ring R] {M : matrix m m R} (hM : M.nondegenerate) {v : m → R} (hv : ∀ (w : m → R), matrix.dot_product v (M.mul_vec 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] [comm_ring R] {M : matrix m m R} (hM : M.nondegenerate) {v : m → R} (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] [comm_ring A] [is_domain A] [decidable_eq m] {M : matrix m m A} (hM : M.det ≠ 0) :

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

See also bilin_form.nondegenerate_of_det_ne_zero' and bilin_form.nondegenerate_of_det_ne_zero.

theorem matrix.eq_zero_of_vec_mul_eq_zero {m : Type u_1} {A : Type u_3} [fintype m] [comm_ring A] [is_domain A] [decidable_eq m] {M : matrix m m A} (hM : M.det ≠ 0) {v : m → A} (hv : matrix.vec_mul v M = 0) :

v = 0

theorem matrix.eq_zero_of_mul_vec_eq_zero {m : Type u_1} {A : Type u_3} [fintype m] [comm_ring A] [is_domain A] [decidable_eq m] {M : matrix m m A} (hM : M.det ≠ 0) {v : m → A} (hv : M.mul_vec v = 0) :

v = 0