theorem
nondeg_fst_of_orthogonalSum_nondeg
{k : Type u_1}
[Field k]
{V₁ : Type u_2}
{V₂ : Type u_3}
[AddCommGroup V₁]
[Module k V₁]
[AddCommGroup V₂]
[Module k V₂]
(B₁ : LinearMap.BilinForm k V₁)
(B₂ : LinearMap.BilinForm k V₂)
(h : Garrett.BilinForm.IsNondegenerate' (Garrett.BilinForm.orthogonalSum B₁ B₂))
:
Nondegeneracy of an orthogonal direct sum B₁ ⊕ B₂ implies nondegeneracy
of the first summand B₁.