theorem
Garrett.orthogonal_le_of_isotropic_of_finrank_ge
{k : Type u_1}
[Field k]
{V : Type u_2}
[AddCommGroup V]
[Module k V]
[FiniteDimensional k V]
(B : LinearMap.BilinForm k V)
(W₁ : Submodule k V)
(hB_nd : B.Nondegenerate)
(hW₁_iso : ∀ w₁ ∈ W₁, ∀ w₂ ∈ W₁, (B w₁) w₂ = 0)
(hW₁_dim : Module.finrank k V ≤ 2 * Module.finrank k ↥W₁)
:
A totally isotropic subspace W₁ whose dimension is at least half of V is
maximal: its orthogonal complement is contained in W₁.
theorem
Garrett.orthogonal_le_of_isotropic_of_finrank_ge'
{k : Type u_1}
[Field k]
{V : Type u_2}
[AddCommGroup V]
[Module k V]
[FiniteDimensional k V]
(B : LinearMap.BilinForm k V)
(W₁ : Submodule k V)
(hB_nd : BilinForm.IsNondegenerate' B)
(hW₁_iso : ∀ w₁ ∈ W₁, ∀ w₂ ∈ W₁, (B w₁) w₂ = 0)
(hW₁_dim : Module.finrank k V ≤ 2 * Module.finrank k ↥W₁)
:
Variant of orthogonal_le_of_isotropic_of_finrank_ge taking the
orthogonal-complement form of nondegeneracy (IsNondegenerate').