internlm/Lean-Github huggingface dataset:
Theorem: QuadraticForm.ex
Proof state before:
case pos
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.130041
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q : QuadraticForm ℚ V
h : FiniteDimensional.finrank ℚ V = 2
hQ : BilinForm.Nondegenerate (↑associated Q)
⊢ HasseMinkowski Q

case neg
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.130041
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q : QuadraticForm ℚ V
h : FiniteDimensional.finrank ℚ V = 2
hQ : ¬BilinForm.Nondegenerate (↑associated Q)
⊢ HasseMinkowski Q
Tactic:
. obtain ⟨w, hw1, hw0, hEQ⟩ := equivalent_weightedSumSquares_units_of_nondegenerate'' Q (by simp [h]) h.symm hQ have := HasseMinkowski_of_Equivalent (V := V) hEQ
  rw [this]
  rw [HasseMinkowski, Isotropic, EverywhereLocallyIsotropic, Isotropic]
  simp at *
  sorry
Proof state after:
case neg
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.130041
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q : QuadraticForm ℚ V
h : FiniteDimensional.finrank ℚ V = 2
hQ : ¬BilinForm.Nondegenerate (↑associated Q)
⊢ HasseMinkowski Q
Theorem: QuadraticForm.ex
Proof state before:
case neg
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.130041
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q : QuadraticForm ℚ V
h : FiniteDimensional.finrank ℚ V = 2
hQ : ¬BilinForm.Nondegenerate (↑associated Q)
⊢ HasseMinkowski Q
Tactic:
. exact HasseMinkowski_of_degenerate Q hQ
Proof state after:
no goals
Theorem: QuadraticForm.ex
Proof state before:
case pos
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.130041
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q : QuadraticForm ℚ V
h : FiniteDimensional.finrank ℚ V = 2
hQ : BilinForm.Nondegenerate (↑associated Q)
⊢ HasseMinkowski Q
Tactic:
obtain ⟨w, hw1, hw0, hEQ⟩ := equivalent_weightedSumSquares_units_of_nondegenerate'' Q (by simp [h]) h.symm hQ
Proof state after:
case pos.intro.intro.intro
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.130041
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q : QuadraticForm ℚ V
h : FiniteDimensional.finrank ℚ V = 2
hQ : BilinForm.Nondegenerate (↑associated Q)
w : Fin 2 → ℤ
hw1 : w { val := 0, isLt := (_ : 0 < 2) } = 1
hw0 : ∀ (i : Fin 2), Squarefree (w i)
hEQ : Equivalent Q (weightedSumSquares ℚ w)
⊢ HasseMinkowski Q
Theorem: QuadraticForm.ex
Proof state before:
case pos.intro.intro.intro
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.130041
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q : QuadraticForm ℚ V
h : FiniteDimensional.finrank ℚ V = 2
hQ : BilinForm.Nondegenerate (↑associated Q)
w : Fin 2 → ℤ
hw1 : w { val := 0, isLt := (_ : 0 < 2) } = 1
hw0 : ∀ (i : Fin 2), Squarefree (w i)
hEQ : Equivalent Q (weightedSumSquares ℚ w)
⊢ HasseMinkowski Q
Tactic:
have := HasseMinkowski_of_Equivalent (V := V) hEQ
Proof state after:
case pos.intro.intro.intro
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.130041
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q : QuadraticForm ℚ V
h : FiniteDimensional.finrank ℚ V = 2
hQ : BilinForm.Nondegenerate (↑associated Q)
w : Fin 2 → ℤ
hw1 : w { val := 0, isLt := (_ : 0 < 2) } = 1
hw0 : ∀ (i : Fin 2), Squarefree (w i)
hEQ : Equivalent Q (weightedSumSquares ℚ w)
this : HasseMinkowski Q ↔ HasseMinkowski (weightedSumSquares ℚ w)
⊢ HasseMinkowski Q
Theorem: QuadraticForm.ex
Proof state before:
case pos.intro.intro.intro
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.130041
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q : QuadraticForm ℚ V
h : FiniteDimensional.finrank ℚ V = 2
hQ : BilinForm.Nondegenerate (↑associated Q)
w : Fin 2 → ℤ
hw1 : w { val := 0, isLt := (_ : 0 < 2) } = 1
hw0 : ∀ (i : Fin 2), Squarefree (w i)
hEQ : Equivalent Q (weightedSumSquares ℚ w)
this : HasseMinkowski Q ↔ HasseMinkowski (weightedSumSquares ℚ w)
⊢ HasseMinkowski Q
Tactic:
rw [this]
Proof state after:
case pos.intro.intro.intro
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.130041
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q : QuadraticForm ℚ V
h : FiniteDimensional.finrank ℚ V = 2
hQ : BilinForm.Nondegenerate (↑associated Q)
w : Fin 2 → ℤ
hw1 : w { val := 0, isLt := (_ : 0 < 2) } = 1
hw0 : ∀ (i : Fin 2), Squarefree (w i)
hEQ : Equivalent Q (weightedSumSquares ℚ w)
this : HasseMinkowski Q ↔ HasseMinkowski (weightedSumSquares ℚ w)
⊢ HasseMinkowski (weightedSumSquares ℚ w)
Theorem: QuadraticForm.ex
Proof state before:
case pos.intro.intro.intro
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.130041
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q : QuadraticForm ℚ V
h : FiniteDimensional.finrank ℚ V = 2
hQ : BilinForm.Nondegenerate (↑associated Q)
w : Fin 2 → ℤ
hw1 : w { val := 0, isLt := (_ : 0 < 2) } = 1
hw0 : ∀ (i : Fin 2), Squarefree (w i)
hEQ : Equivalent Q (weightedSumSquares ℚ w)
this : HasseMinkowski Q ↔ HasseMinkowski (weightedSumSquares ℚ w)
⊢ HasseMinkowski (weightedSumSquares ℚ w)
Tactic:
rw [HasseMinkowski, Isotropic, EverywhereLocallyIsotropic, Isotropic]
Proof state after:
case pos.intro.intro.intro
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.130041
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q : QuadraticForm ℚ V
h : FiniteDimensional.finrank ℚ V = 2
hQ : BilinForm.Nondegenerate (↑associated Q)
w : Fin 2 → ℤ
hw1 : w { val := 0, isLt := (_ : 0 < 2) } = 1
hw0 : ∀ (i : Fin 2), Squarefree (w i)
hEQ : Equivalent Q (weightedSumSquares ℚ w)
this : HasseMinkowski Q ↔ HasseMinkowski (weightedSumSquares ℚ w)
⊢ ¬Anisotropic (weightedSumSquares ℚ w) ↔
    (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Isotropic (baseChange ℚ_[p] (weightedSumSquares ℚ w))) ∧
      ¬Anisotropic (baseChange ℝ (weightedSumSquares ℚ w))
Theorem: QuadraticForm.ex
Proof state before:
case pos.intro.intro.intro
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.130041
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q : QuadraticForm ℚ V
h : FiniteDimensional.finrank ℚ V = 2
hQ : BilinForm.Nondegenerate (↑associated Q)
w : Fin 2 → ℤ
hw1 : w { val := 0, isLt := (_ : 0 < 2) } = 1
hw0 : ∀ (i : Fin 2), Squarefree (w i)
hEQ : Equivalent Q (weightedSumSquares ℚ w)
this : HasseMinkowski Q ↔ HasseMinkowski (weightedSumSquares ℚ w)
⊢ ¬Anisotropic (weightedSumSquares ℚ w) ↔
    (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Isotropic (baseChange ℚ_[p] (weightedSumSquares ℚ w))) ∧
      ¬Anisotropic (baseChange ℝ (weightedSumSquares ℚ w))
Tactic:
simp at *
Proof state after:
case pos.intro.intro.intro
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.130041
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q : QuadraticForm ℚ V
h : FiniteDimensional.finrank ℚ V = 2
hQ : BilinForm.Nondegenerate (↑associated Q)
w : Fin 2 → ℤ
hw1 : w 0 = 1
hw0 : ∀ (i : Fin 2), Squarefree (w i)
hEQ : Equivalent Q (weightedSumSquares ℚ w)
this : HasseMinkowski Q ↔ HasseMinkowski (weightedSumSquares ℚ w)
⊢ ¬Anisotropic (weightedSumSquares ℚ w) ↔
    (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Isotropic (baseChange ℚ_[p] (weightedSumSquares ℚ w))) ∧
      ¬Anisotropic (baseChange ℝ (weightedSumSquares ℚ w))
Theorem: QuadraticForm.ex
Proof state before:
case pos.intro.intro.intro
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.130041
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q : QuadraticForm ℚ V
h : FiniteDimensional.finrank ℚ V = 2
hQ : BilinForm.Nondegenerate (↑associated Q)
w : Fin 2 → ℤ
hw1 : w 0 = 1
hw0 : ∀ (i : Fin 2), Squarefree (w i)
hEQ : Equivalent Q (weightedSumSquares ℚ w)
this : HasseMinkowski Q ↔ HasseMinkowski (weightedSumSquares ℚ w)
⊢ ¬Anisotropic (weightedSumSquares ℚ w) ↔
    (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Isotropic (baseChange ℚ_[p] (weightedSumSquares ℚ w))) ∧
      ¬Anisotropic (baseChange ℝ (weightedSumSquares ℚ w))
Tactic:
sorry
Proof state after:
no goals
Theorem: QuadraticForm.ex
Proof state before:
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.130041
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q : QuadraticForm ℚ V
h : FiniteDimensional.finrank ℚ V = 2
hQ : BilinForm.Nondegenerate (↑associated Q)
⊢ 0 < FiniteDimensional.finrank ℚ V
Tactic:
simp [h]
Proof state after:
no goals
Theorem: QuadraticForm.ex
Proof state before:
case neg
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.130041
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q : QuadraticForm ℚ V
h : FiniteDimensional.finrank ℚ V = 2
hQ : ¬BilinForm.Nondegenerate (↑associated Q)
⊢ HasseMinkowski Q
Tactic:
exact HasseMinkowski_of_degenerate Q hQ
Proof state after:
no goals
Theorem: QuadraticForm.weightedSumSquares_basechange_anisotropic_iff
Proof state before:
V : Type ?u.142725
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.143267
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
a p : ℕ
w : Fin a → ℤ
hp : Fact (Nat.Prime p)
⊢ Anisotropic (baseChange ℚ_[p] (weightedSumSquares ℚ w)) ↔ Anisotropic (weightedSumSquares ℚ_[p] fun i => ↑(w i))
Tactic:
sorry
Proof state after:
no goals
Theorem: QuadraticForm.HasseMinkowski2
Proof state before:
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
⊢ HasseMinkowski F
Tactic:
by_cases hF : (associated (R₁ := ℚ) F).Nondegenerate
Proof state after:
case pos
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)
⊢ HasseMinkowski F

case neg
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)
⊢ HasseMinkowski F
Theorem: QuadraticForm.HasseMinkowski2
Proof state before:
case pos
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)
⊢ HasseMinkowski F
Tactic:
have hV0 : 0 < FiniteDimensional.finrank ℚ V := by rw [hV]; norm_num
Proof state after:
case pos
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
⊢ HasseMinkowski F
Theorem: QuadraticForm.HasseMinkowski2
Proof state before:
case pos
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
⊢ HasseMinkowski F
Tactic:
obtain ⟨w, hw1, hw0, hEF⟩ := equivalent_weightedSumSquares_units_of_nondegenerate'' F hV0 hV.symm hF
Proof state after:
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)
⊢ HasseMinkowski F
Theorem: QuadraticForm.HasseMinkowski2
Proof state before:
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)
⊢ HasseMinkowski F
Tactic:
rw [HasseMinkowski_of_Equivalent (V := V) hEF, HasseMinkowski]
Proof state after:
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)
Theorem: QuadraticForm.HasseMinkowski2
Proof state before:
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)
Tactic:
constructor
Proof state after:
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)
Theorem: QuadraticForm.HasseMinkowski2
Proof state before:
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)
⊢ 0 < FiniteDimensional.finrank ℚ V
Tactic:
rw [hV]
Proof state after:
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)
⊢ 0 < 2
Theorem: QuadraticForm.HasseMinkowski2
Proof state before:
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)
⊢ 0 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: QuadraticForm.HasseMinkowski2
Proof state before:
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)
Tactic:
intro h
Proof state after:
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)
h : Isotropic (weightedSumSquares ℚ w)
⊢ EverywhereLocallyIsotropic (weightedSumSquares ℚ w)
Theorem: QuadraticForm.HasseMinkowski2
Proof state before:
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)
h : Isotropic (weightedSumSquares ℚ w)
⊢ EverywhereLocallyIsotropic (weightedSumSquares ℚ w)
Tactic:
exact HasseMinkowski_global_to_local _ h
Proof state after:
no goals
Theorem: QuadraticForm.HasseMinkowski2
Proof state before:
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)
Tactic:
intro hl
Proof state after:
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)
hl : EverywhereLocallyIsotropic (weightedSumSquares ℚ w)
⊢ Isotropic (weightedSumSquares ℚ w)
Theorem: QuadraticForm.HasseMinkowski2
Proof state before:
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)
hl : EverywhereLocallyIsotropic (weightedSumSquares ℚ w)
⊢ Isotropic (weightedSumSquares ℚ w)
Tactic:
by_cases hw : w ⟨1, (by norm_num)⟩ = -1
Proof state after:
case pos
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)
hl : EverywhereLocallyIsotropic (weightedSumSquares ℚ w)
hw : w { val := 1, isLt := (_ : 1 < 2) } = -1
⊢ Isotropic (weightedSumSquares ℚ w)

case neg
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)
hl : EverywhereLocallyIsotropic (weightedSumSquares ℚ w)
hw : ¬w { val := 1, isLt := (_ : 1 < 2) } = -1
⊢ Isotropic (weightedSumSquares ℚ w)