internlm/Lean-Github huggingface dataset:
Theorem: QuadraticForm.anisotropic_of_Equivalent
Proof state before:
case intro
ι : Type ?u.84107
R✝ : Type ?u.84110
K : Type ?u.84113
M✝ : Type ?u.84116
M₁ : Type ?u.84119
M₂ : Type u_1
M₃ : Type ?u.84125
V : Type ?u.84128
R : Type u_2
M : Type u_3
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : FiniteDimensional R M
inst✝² : Invertible 2
Q✝ : QuadraticForm R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
x : M₂
hx : ↑S x = 0
h : ↑Q (↑(Isometry.symm val) x) = 0 → ↑(Isometry.symm val) x = 0
⊢ x = 0
Tactic:
simp only [Isometry.map_app, AddEquivClass.map_eq_zero_iff] at h
Proof state after:
case intro
ι : Type ?u.84107
R✝ : Type ?u.84110
K : Type ?u.84113
M✝ : Type ?u.84116
M₁ : Type ?u.84119
M₂ : Type u_1
M₃ : Type ?u.84125
V : Type ?u.84128
R : Type u_2
M : Type u_3
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : FiniteDimensional R M
inst✝² : Invertible 2
Q✝ : QuadraticForm R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
x : M₂
hx : ↑S x = 0
h : ↑S x = 0 → x = 0
⊢ x = 0
Theorem: QuadraticForm.anisotropic_of_Equivalent
Proof state before:
case intro
ι : Type ?u.84107
R✝ : Type ?u.84110
K : Type ?u.84113
M✝ : Type ?u.84116
M₁ : Type ?u.84119
M₂ : Type u_1
M₃ : Type ?u.84125
V : Type ?u.84128
R : Type u_2
M : Type u_3
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : FiniteDimensional R M
inst✝² : Invertible 2
Q✝ : QuadraticForm R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
x : M₂
hx : ↑S x = 0
h : ↑S x = 0 → x = 0
⊢ x = 0
Tactic:
specialize h hx
Proof state after:
case intro
ι : Type ?u.84107
R✝ : Type ?u.84110
K : Type ?u.84113
M✝ : Type ?u.84116
M₁ : Type ?u.84119
M₂ : Type u_1
M₃ : Type ?u.84125
V : Type ?u.84128
R : Type u_2
M : Type u_3
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : FiniteDimensional R M
inst✝² : Invertible 2
Q✝ : QuadraticForm R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
x : M₂
hx : ↑S x = 0
h : x = 0
⊢ x = 0
Theorem: QuadraticForm.anisotropic_of_Equivalent
Proof state before:
case intro
ι : Type ?u.84107
R✝ : Type ?u.84110
K : Type ?u.84113
M✝ : Type ?u.84116
M₁ : Type ?u.84119
M₂ : Type u_1
M₃ : Type ?u.84125
V : Type ?u.84128
R : Type u_2
M : Type u_3
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : FiniteDimensional R M
inst✝² : Invertible 2
Q✝ : QuadraticForm R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
x : M₂
hx : ↑S x = 0
h : x = 0
⊢ x = 0
Tactic:
simpa using h
Proof state after:
no goals
Theorem: QuadraticForm.equivalent_weightedSumSquares_units_of_nondegenerate''
Proof state before:
ι : Type ?u.120511
R✝ : Type ?u.120514
K : Type ?u.120517
M✝ : Type ?u.120520
M₁ : Type ?u.120523
M₂ : Type ?u.120526
M₃ : Type ?u.120529
V : Type u_1
R : Type ?u.120535
M : Type ?u.120538
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : FiniteDimensional R M
inst✝² : Invertible 2
Q✝ : QuadraticForm R M
inst✝¹ : AddCommGroup V
inst✝ : Module ℚ V
a : ℕ
Q : QuadraticForm ℚ V
h : 0 < FiniteDimensional.finrank ℚ V
ha : a = FiniteDimensional.finrank ℚ V
hQ : BilinForm.Nondegenerate (↑associated Q)
⊢ ∃ w hw1 hw0, Equivalent Q (weightedSumSquares ℚ w)
Tactic:
sorry
Proof state after:
no goals
Theorem: QuadraticForm.Isotropic_of_zero_quadForm_dim_ge1
Proof state before:
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
Tactic:
rw [QuadraticForm.Isotropic]
Proof state after:
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
Theorem: QuadraticForm.Isotropic_of_zero_quadForm_dim_ge1
Proof state before:
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
Tactic:
rw [QuadraticForm.Anisotropic]
Proof state after:
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
⊢ ¬∀ (x : W), ↑Q x = 0 → x = 0
Theorem: QuadraticForm.Isotropic_of_zero_quadForm_dim_ge1
Proof state before:
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
⊢ ¬∀ (x : W), ↑Q x = 0 → x = 0
Tactic:
have h: ∃ (w : W), w ≠ 0 := by
  simpa only [ne_eq, rank_zero_iff_forall_zero, not_forall] using h₂
Proof state after:
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
h : ∃ w, w ≠ 0
⊢ ¬∀ (x : W), ↑Q x = 0 → x = 0
Theorem: QuadraticForm.Isotropic_of_zero_quadForm_dim_ge1
Proof state before:
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
h : ∃ w, w ≠ 0
⊢ ¬∀ (x : W), ↑Q x = 0 → x = 0
Tactic:
obtain ⟨w, hw⟩ := h
Proof state after:
case intro
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
w : W
hw : w ≠ 0
⊢ ¬∀ (x : W), ↑Q x = 0 → x = 0
Theorem: QuadraticForm.Isotropic_of_zero_quadForm_dim_ge1
Proof state before:
case intro
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
w : W
hw : w ≠ 0
⊢ ¬∀ (x : W), ↑Q x = 0 → x = 0
Tactic:
have : Q w = 0 := by
  rw [h₁]
  simp only [zero_apply]
Proof state after:
case intro
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
w : W
hw : w ≠ 0
this : ↑Q w = 0
⊢ ¬∀ (x : W), ↑Q x = 0 → x = 0
Theorem: QuadraticForm.Isotropic_of_zero_quadForm_dim_ge1
Proof state before:
case intro
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
w : W
hw : w ≠ 0
this : ↑Q w = 0
⊢ ¬∀ (x : W), ↑Q x = 0 → x = 0
Tactic:
tauto
Proof state after:
no goals
Theorem: QuadraticForm.Isotropic_of_zero_quadForm_dim_ge1
Proof state before:
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
⊢ ∃ w, w ≠ 0
Tactic:
simpa only [ne_eq, rank_zero_iff_forall_zero, not_forall] using h₂
Proof state after:
no goals
Theorem: QuadraticForm.Isotropic_of_zero_quadForm_dim_ge1
Proof state before:
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
w : W
hw : w ≠ 0
⊢ ↑Q w = 0
Tactic:
rw [h₁]
Proof state after:
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
w : W
hw : w ≠ 0
⊢ ↑0 w = 0
Theorem: QuadraticForm.Isotropic_of_zero_quadForm_dim_ge1
Proof state before:
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
w : W
hw : w ≠ 0
⊢ ↑0 w = 0
Tactic:
simp only [zero_apply]
Proof state after:
no goals
Theorem: QuadraticForm.anisotropic_of_quadForm_dim_zero
Proof state before:
V : Type ?u.23522
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 : Module.rank k W = 0
⊢ Anisotropic Q
Tactic:
intro (w : W)
Proof state after:
V : Type ?u.23522
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 : Module.rank k W = 0
w : W
⊢ ↑Q w = 0 → w = 0
Theorem: QuadraticForm.anisotropic_of_quadForm_dim_zero
Proof state before:
V : Type ?u.23522
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 : Module.rank k W = 0
w : W
⊢ ↑Q w = 0 → w = 0
Tactic:
intro
Proof state after:
V : Type ?u.23522
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 : Module.rank k W = 0
w : W
a✝ : ↑Q w = 0
⊢ w = 0
Theorem: QuadraticForm.anisotropic_of_quadForm_dim_zero
Proof state before:
V : Type ?u.23522
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 : Module.rank k W = 0
w : W
a✝ : ↑Q w = 0
⊢ w = 0
Tactic:
rw [rank_zero_iff_forall_zero] at h
Proof state after:
V : Type ?u.23522
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 : ∀ (x : W), x = 0
w : W
a✝ : ↑Q w = 0
⊢ w = 0
Theorem: QuadraticForm.anisotropic_of_quadForm_dim_zero
Proof state before:
V : Type ?u.23522
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 : ∀ (x : W), x = 0
w : W
a✝ : ↑Q w = 0
⊢ w = 0
Tactic:
exact h w
Proof state after:
no goals
Theorem: QuadraticForm.Hasse_Minkowski0
Proof 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
hV : Module.rank ℚ V = 0
⊢ ∀ (F : QuadraticForm ℚ V), Hasse_Minkowski F
Tactic:
intro F
Proof state after:
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
⊢ Hasse_Minkowski F
Theorem: QuadraticForm.Hasse_Minkowski0
Proof 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
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
⊢ Hasse_Minkowski F
Tactic:
rw [Hasse_Minkowski]
Proof state after:
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
⊢ Isotropic F ↔ EverywhereLocallyIsotropic F
Theorem: QuadraticForm.Hasse_Minkowski0
Proof 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
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
⊢ Isotropic F ↔ EverywhereLocallyIsotropic F
Tactic:
constructor
Proof state after:
case mp
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
⊢ Isotropic F → EverywhereLocallyIsotropic F

case mpr
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
⊢ EverywhereLocallyIsotropic F → Isotropic F
Theorem: QuadraticForm.Hasse_Minkowski0
Proof state before:
case mp
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
⊢ Isotropic F → EverywhereLocallyIsotropic F
Tactic:
contrapose
Proof state after:
case mp
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
⊢ ¬EverywhereLocallyIsotropic F → ¬Isotropic F
Theorem: QuadraticForm.Hasse_Minkowski0
Proof state before:
case mp
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
⊢ ¬EverywhereLocallyIsotropic F → ¬Isotropic F
Tactic:
intro
Proof state after:
case mp
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
a✝ : ¬EverywhereLocallyIsotropic F
⊢ ¬Isotropic F
Theorem: QuadraticForm.Hasse_Minkowski0
Proof state before:
case mp
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
a✝ : ¬EverywhereLocallyIsotropic F
⊢ ¬Isotropic F
Tactic:
rw [QuadraticForm.Isotropic]
Proof state after:
case mp
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
a✝ : ¬EverywhereLocallyIsotropic F
⊢ ¬¬Anisotropic F
Theorem: QuadraticForm.Hasse_Minkowski0
Proof state before:
case mp
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
a✝ : ¬EverywhereLocallyIsotropic F
⊢ ¬¬Anisotropic F
Tactic:
simp only [not_not]
Proof state after:
case mp
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
a✝ : ¬EverywhereLocallyIsotropic F
⊢ Anisotropic F
Theorem: QuadraticForm.Hasse_Minkowski0
Proof state before:
case mp
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
a✝ : ¬EverywhereLocallyIsotropic F
⊢ Anisotropic F
Tactic:
apply anisotropic_of_quadForm_dim_zero _ _ F hV
Proof state after:
no goals
Theorem: QuadraticForm.Hasse_Minkowski0
Proof state before:
case mpr
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
⊢ EverywhereLocallyIsotropic F → Isotropic F
Tactic:
contrapose
Proof state after:
case mpr
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
⊢ ¬Isotropic F → ¬EverywhereLocallyIsotropic F
Theorem: QuadraticForm.Hasse_Minkowski0
Proof state before:
case mpr
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
⊢ ¬Isotropic F → ¬EverywhereLocallyIsotropic F
Tactic:
intro
Proof state after:
case mpr
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
a✝ : ¬Isotropic F
⊢ ¬EverywhereLocallyIsotropic F
Theorem: QuadraticForm.Hasse_Minkowski0
Proof state before:
case mpr
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
a✝ : ¬Isotropic F
⊢ ¬EverywhereLocallyIsotropic F
Tactic:
rw [QuadraticForm.EverywhereLocallyIsotropic]
Proof state after:
case mpr
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
a✝ : ¬Isotropic F
⊢ ¬((∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Isotropic (baseChange ℚ_[p] F)) ∧ Isotropic (baseChange ℝ F))
Theorem: QuadraticForm.Hasse_Minkowski0
Proof state before:
case mpr
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
a✝ : ¬Isotropic F
⊢ ¬((∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Isotropic (baseChange ℚ_[p] F)) ∧ Isotropic (baseChange ℝ F))
Tactic:
push_neg
Proof state after:
case mpr
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
a✝ : ¬Isotropic F
⊢ (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Isotropic (baseChange ℚ_[p] F)) → ¬Isotropic (baseChange ℝ F)
Theorem: QuadraticForm.Hasse_Minkowski0
Proof state before:
case mpr
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
a✝ : ¬Isotropic F
⊢ (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Isotropic (baseChange ℚ_[p] F)) → ¬Isotropic (baseChange ℝ F)
Tactic:
intro
Proof state after:
case mpr
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
a✝ : ¬Isotropic F
_✝ : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Isotropic (baseChange ℚ_[p] F)
⊢ ¬Isotropic (baseChange ℝ F)
Theorem: QuadraticForm.Hasse_Minkowski0
Proof state before:
case mpr
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
a✝ : ¬Isotropic F
_✝ : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Isotropic (baseChange ℚ_[p] F)
⊢ ¬Isotropic (baseChange ℝ F)
Tactic:
simp only [not_not]
Proof state after:
case mpr
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
a✝ : ¬Isotropic F
_✝ : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Isotropic (baseChange ℚ_[p] F)
⊢ Anisotropic (baseChange ℝ F)
Theorem: QuadraticForm.Hasse_Minkowski0
Proof state before:
case mpr
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
a✝ : ¬Isotropic F
_✝ : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Isotropic (baseChange ℚ_[p] F)
⊢ Anisotropic (baseChange ℝ F)
Tactic:
apply anisotropic_of_quadForm_dim_zero
Proof state after:
case mpr.h
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
a✝ : ¬Isotropic F
_✝ : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Isotropic (baseChange ℚ_[p] F)
⊢ Module.rank ℝ (TensorProduct ℚ ℝ V) = 0
Theorem: QuadraticForm.Hasse_Minkowski0
Proof state before:
case mpr.h
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
hV : Module.rank ℚ V = 0
F : QuadraticForm ℚ V
a✝ : ¬Isotropic F
_✝ : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Isotropic (baseChange ℚ_[p] F)
⊢ Module.rank ℝ (TensorProduct ℚ ℝ V) = 0
Tactic:
rw [← base_change_module_rank_preserved, hV]
Proof state after:
no goals
Theorem: QuadraticForm.Hasse_Minkowski_of_Equivalent
Proof 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 S : QuadraticForm ℚ V
h : Equivalent Q S
⊢ Hasse_Minkowski Q ↔ Hasse_Minkowski S
Tactic:
simp only [Hasse_Minkowski, Isotropic, EverywhereLocallyIsotropic] at *
Proof state after:
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q S : QuadraticForm ℚ V
h : Equivalent Q S
⊢ (¬Anisotropic Q ↔
      (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ¬Anisotropic (baseChange ℚ_[p] Q)) ∧ ¬Anisotropic (baseChange ℝ Q)) ↔
    (¬Anisotropic S ↔
      (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ¬Anisotropic (baseChange ℚ_[p] S)) ∧ ¬Anisotropic (baseChange ℝ S))
Theorem: QuadraticForm.Hasse_Minkowski_of_Equivalent
Proof 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 S : QuadraticForm ℚ V
h : Equivalent Q S
⊢ (¬Anisotropic Q ↔
      (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ¬Anisotropic (baseChange ℚ_[p] Q)) ∧ ¬Anisotropic (baseChange ℝ Q)) ↔
    (¬Anisotropic S ↔
      (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ¬Anisotropic (baseChange ℚ_[p] S)) ∧ ¬Anisotropic (baseChange ℝ S))
Tactic:
simp only [anisotropic_iff _ _ h]
Proof state after:
V : Type
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℚ V
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q S : QuadraticForm ℚ V
h : Equivalent Q S
⊢ (¬Anisotropic S ↔
      (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ¬Anisotropic (baseChange ℚ_[p] Q)) ∧ ¬Anisotropic (baseChange ℝ Q)) ↔
    (¬Anisotropic S ↔
      (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ¬Anisotropic (baseChange ℚ_[p] S)) ∧ ¬Anisotropic (baseChange ℝ S))