theorem Formalization.GeometricAlgebra.hyperbolic_spaces_of_same_dim_isometric {k : Type u_1} [Field k] [Invertible 2] {V₁ : Type u_2} {V₂ : Type u_3} [AddCommGroup V₁] [Module k V₁] [FiniteDimensional k V₁] [AddCommGroup V₂] [Module k V₂] [FiniteDimensional k V₂] (B₁ : LinearMap.BilinForm k V₁) (B₂ : LinearMap.BilinForm k V₂) (hHyp₁ : Garrett.BilinForm.IsHyperbolic B₁) (hHyp₂ : Garrett.BilinForm.IsHyperbolic B₂) (hdim : Module.finrank k V₁ = Module.finrank k V₂) : Garrett.FormedSpacesIsometric B₁ B₂

Two hyperbolic formed spaces of the same finite dimension are isometric. NOTE: the proof of this statement is currently sorry.

theorem Formalization.GeometricAlgebra.isAlt_skew {k : Type u_1} [Field k] [Invertible 2] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (hAlt : B.IsAlt) (x y : V) : (B x) y = -(B y) x

An alternating bilinear form is skew-symmetric: B x y = -(B y x).