Matrices associated with non-degenerate bilinear forms #
Main definitions #
matrix.nondegenerate A: the proposition that when interpreted as a bilinear form, the matrixAis nondegenerate.
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), 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