constructor
case pos.intro.intro.intro
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.151517
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : FiniteDimensional.finrank ℚ V = 2
F : QuadraticForm ℚ V
hF : BilinForm.Nondegenerate (↑associated F)
hV0 : 0 < FiniteDimensional.finrank ℚ V
w : Fin 2 → ℤ
hw1 : w { val := 0, isLt := (_ : 0 < 2) } = 1
hw0 : ∀ (i : Fin 2), Squarefree (w i)
hEF : Equivalent F (weightedSumSquares ℚ w)
⊢ Isotropic (weightedSumSquares ℚ w) ↔ EverywhereLocallyIsotropic (weightedSumSquares ℚ w)
case pos.intro.intro.intro.mp
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.151517
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : FiniteDimensional.finrank ℚ V = 2
F : QuadraticForm ℚ V
hF : BilinForm.Nondegenerate (↑associated F)
hV0 : 0 < FiniteDimensional.finrank ℚ V
w : Fin 2 → ℤ
hw1 : w { val := 0, isLt := (_ : 0 < 2) } = 1
hw0 : ∀ (i : Fin 2), Squarefree (w i)
hEF : Equivalent F (weightedSumSquares ℚ w)
⊢ Isotropic (weightedSumSquares ℚ w) → EverywhereLocallyIsotropic (weightedSumSquares ℚ w)

case pos.intro.intro.intro.mpr
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.151517
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : FiniteDimensional.finrank ℚ V = 2
F : QuadraticForm ℚ V
hF : BilinForm.Nondegenerate (↑associated F)
hV0 : 0 < FiniteDimensional.finrank ℚ V
w : Fin 2 → ℤ
hw1 : w { val := 0, isLt := (_ : 0 < 2) } = 1
hw0 : ∀ (i : Fin 2), Squarefree (w i)
hEF : Equivalent F (weightedSumSquares ℚ w)
⊢ EverywhereLocallyIsotropic (weightedSumSquares ℚ w) → Isotropic (weightedSumSquares ℚ w)