theorem Garrett.nondegenerate_iff_compl {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (B : LinearMap.BilinForm k V) (hBrefl : B.IsRefl) (U : Submodule k V) : (B.restrict U).Nondegenerate ↔ IsCompl U (B.orthogonal U)

The restriction of a reflexive bilinear form to a subspace U is nondegenerate iff U and its orthogonal complement form a direct sum.

theorem Garrett.nondegenerate_iff_orthogonal_nondegenerate {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (B : LinearMap.BilinForm k V) (hBnd : B.Nondegenerate) (hBrefl : B.IsRefl) (U : Submodule k V) : (B.restrict U).Nondegenerate ↔ (B.restrict (B.orthogonal U)).Nondegenerate

The restriction of B to U is nondegenerate iff its restriction to the orthogonal complement Uᗮ is nondegenerate.

theorem Garrett.compl_iff_orthogonal_nondegenerate {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (B : LinearMap.BilinForm k V) (hBnd : B.Nondegenerate) (hBrefl : B.IsRefl) (U : Submodule k V) : IsCompl U (B.orthogonal U) ↔ (B.restrict (B.orthogonal U)).Nondegenerate

U and Uᗮ form a direct sum iff the restriction of B to Uᗮ is nondegenerate.