theorem Garrett.wittExtension_bot {k : Type u_1} [CommRing k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (_hnd : B.orthogonal ⊤ = ⊥) (W : Submodule k V) (φ : ↥⊥ ≃ₗ[k] ↥W) (_hφ : IsSubspaceIsometry B ⊥ W φ) : ∃ (Φ : V ≃ₗ[k] V), (∀ (v₁ v₂ : V), (B (Φ v₁)) (Φ v₂) = (B v₁) v₂) ∧ ∀ (u : ↥⊥), Φ ↑u = ↑(φ u)

Trivial case of Witt's extension theorem: any isometry from the zero subspace extends to the identity automorphism of V.