theorem Garrett.nondegenerate_of_orthogonal_top_eq_bot {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (href : B.IsRefl) (hnd : B.orthogonal ⊤ = ⊥) : B.Nondegenerate

For a reflexive bilinear form B, vanishing of the orthogonal complement of ⊤ implies nondegeneracy.

theorem Garrett.orthogonal_top_eq_bot_of_nondegenerate {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (href : B.IsRefl) (hnd : B.Nondegenerate) : B.orthogonal ⊤ = ⊥

Converse of nondegenerate_of_orthogonal_top_eq_bot: a reflexive nondegenerate form has trivial orthogonal complement of ⊤.

theorem Garrett.isCompl_span_singleton_orthogonal {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) {x : V} (hx : ¬B.IsOrtho x x) : IsCompl (k ∙ x) (B.orthogonal (k ∙ x))

If x is anisotropic for B (i.e. not orthogonal to itself), then k ∙ x and its orthogonal complement are complementary subspaces.

theorem Garrett.restrict_nondegenerate_orthogonal_spanSingleton {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (href : B.IsRefl) (hnd : B.orthogonal ⊤ = ⊥) {x : V} (hx : ¬B.IsOrtho x x) : (B.restrict (B.orthogonal (k ∙ x))).Nondegenerate

The restriction of a reflexive nondegenerate form B to the orthogonal complement of a span of a single anisotropic vector remains nondegenerate.

theorem Garrett.orthogonal_isCompl_of_restrict_nondegenerate {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (B : LinearMap.BilinForm k V) (href : ∀ (x y : V), (B x) y = 0 → (B y) x = 0) (S : Submodule k V) (hS : (B.restrict S).Nondegenerate) : IsCompl S (B.orthogonal S)

For a reflexive form on a finite-dimensional space, a subspace S on which B restricts nondegenerately is complementary to its orthogonal complement.