Theorem: QuadraticForm.HasseMinkowski_of_degenerate (AntLorentz/HasseMinkowski2.lean)

State before:
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q : QuadraticForm ℚ V
hQ : ¬BilinForm.Nondegenerate (↑associated Q)
⊢ Hasse_Minkowski Q
Tactic:
sorry
State after:
no goals