theorem Garrett.anisotropic_hyperbolic_trivial {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (hAniso : BilinForm.IsAnisotropic B) (hHyp : BilinForm.IsHyperbolic B) (v : V) : v = 0

A formed space that is simultaneously anisotropic and hyperbolic must be trivial: every vector is zero.