Linear independence from the Gram matrix of a bilinear form #
A family of vectors whose Gram matrix with respect to a bilinear form has nonzero determinant is
linearly independent, over any commutative ring without zero divisors. A linear relation
∑ x, g x • c x = 0 pairs with every c y to give G *ᵥ g = 0 for the Gram matrix G, and a
square matrix with nonzero determinant has trivial kernel (Matrix.eq_zero_of_mulVec_eq_zero).
Mathlib has the matrix statement but not the bilinear-form criterion.
Main results #
LinearMap.BilinForm.linearIndependent_of_det_ne_zero: a family whose Gram matrix with respect to a bilinear form has nonzero determinant is linearly independent.
theorem
LinearMap.BilinForm.linearIndependent_of_det_ne_zero
{R : Type u_1}
{M : Type u_2}
[CommRing R]
[NoZeroDivisors R]
[AddCommGroup M]
[Module R M]
{ι : Type u_3}
[Fintype ι]
[DecidableEq ι]
(B : LinearMap.BilinForm R M)
{c : ι → M}
(h : (Matrix.of fun (x y : ι) => (B (c x)) (c y)).det ≠ 0)
:
A family whose Gram matrix with respect to a bilinear form has nonzero determinant is linearly independent.