theorem Garrett.finrank_orthogonal_of_IsNondegenerate' {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (B : LinearMap.BilinForm k V) (hB : BilinForm.IsNondegenerate' B) (W : Submodule k V) : Module.finrank k ↥(B.orthogonal W) = Module.finrank k V - Module.finrank k ↥W

For a nondegenerate bilinear form B (in Garrett's sense IsNondegenerate' B) on a finite-dimensional space, the orthogonal complement of a subspace W has dimension dim V − dim W.

theorem Garrett.finrank_orthogonal_of_Nondegenerate' {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] [FiniteDimensional k V] {B : LinearMap.BilinForm k V} (hB : B.Nondegenerate) (W : Submodule k V) : Module.finrank k ↥(B.orthogonal W) = Module.finrank k V - Module.finrank k ↥W

Same dimension formula but stated with the Mathlib Nondegenerate hypothesis: dim (W^⊥) = dim V − dim W for nondegenerate B.

theorem Garrett.finrank_add_finrank_orthogonal_of_IsNondegenerate' {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (B : LinearMap.BilinForm k V) (hB : BilinForm.IsNondegenerate' B) (W : Submodule k V) : Module.finrank k ↥W + Module.finrank k ↥(B.orthogonal W) = Module.finrank k V

Additive form of the dimension formula: for nondegenerate B, the dimensions of W and of its orthogonal complement sum to dim V.