theorem IsNondegenerate'_to_Nondegenerate {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] [FiniteDimensional k V] {B : LinearMap.BilinForm k V} (h : Garrett.BilinForm.IsNondegenerate' B) : B.Nondegenerate

Convert the orthogonal-complement form of nondegeneracy (Garrett.BilinForm.IsNondegenerate') into Mathlib's BilinForm.Nondegenerate.