feat(linear_algebra/bilinear_form): bilinear forms with det ≠ 0 are…

… nonsingular (#8824)

In particular, the trace form is such a bilinear form (see #8777).

src/linear_algebra/bilinear_form.lean

@@ -1576,4 +1576,28 @@ theorem is_adjoint_pair_iff_eq_of_nondegenerate
 
 end linear_adjoints
 
+section det
+
+open matrix
+
+variables {A : Type*} [integral_domain A] [module A M₃] (B₃ : bilin_form A M₃)
+variables {ι : Type*} [decidable_eq ι] [fintype ι]
+
+theorem nondegenerate_of_det_ne_zero' (M : matrix ι ι A) (h : M.det ≠ 0) :
+  (to_bilin' M).nondegenerate :=
+λ x hx, matrix.nondegenerate_of_det_ne_zero h x (λ y,
+  by simpa only [to_bilin'_apply, dot_product, mul_vec, finset.mul_sum, mul_assoc] using hx y)
+
+theorem nondegenerate_of_det_ne_zero (b : basis ι A M₃) (h : (to_matrix b B₃).det ≠ 0) :
+  B₃.nondegenerate :=
+begin
+  intros x hx,
+  refine b.equiv_fun.map_eq_zero_iff.mp (nondegenerate_of_det_ne_zero' _ h _ (λ w, _)),
+  convert hx (b.equiv_fun.symm w),
+  rw [bilin_form.to_matrix, linear_equiv.trans_apply, to_bilin'_to_matrix', congr_apply,
+      linear_equiv.symm_apply_apply]
+end
+
+end det
+
 end bilin_form

src/linear_algebra/matrix/nonsingular_inverse.lean

@@ -491,4 +491,22 @@ divides `b`. -/
   A.mul_vec (cramer A b) = A.det • b :=
 by rw [cramer_eq_adjugate_mul_vec, mul_vec_mul_vec, mul_adjugate, smul_mul_vec_assoc, one_mul_vec]
 
+/-- 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 nondegenerate_of_det_ne_zero {A : Type*} [integral_domain A]
+  {M : matrix n n A} (hM : M.det ≠ 0)
+  (v : n → A) (hv : ∀ w, matrix.dot_product v (mul_vec M w) = 0) : v = 0 :=
+begin
+  ext i,
+  specialize hv (M.cramer (pi.single i 1)),
+  refine (mul_eq_zero.mp _).resolve_right hM,
+  convert hv,
+  simp only [mul_vec_cramer M (pi.single i 1), dot_product, pi.smul_apply, smul_eq_mul],
+  rw [finset.sum_eq_single i, pi.single_eq_same, mul_one],
+  { intros j _ hj, simp [hj] },
+  { intros, have := finset.mem_univ i, contradiction }
+end
+
 end matrix