rw [QuadraticForm.Isotropic]
V : Type ?u.14055
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module ℚ V
inst✝³ : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝² : Field k
inst✝¹ : AddCommGroup W
inst✝ : Module k W
Q : QuadraticForm k W
h₁ : Q = 0
h₂ : Module.rank k W ≠ 0
⊢ Isotropic Q
V : Type ?u.14055
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module ℚ V
inst✝³ : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝² : Field k
inst✝¹ : AddCommGroup W
inst✝ : Module k W
Q : QuadraticForm k W
h₁ : Q = 0
h₂ : Module.rank k W ≠ 0
⊢ ¬Anisotropic Q