Theorem: QuadraticForm.Hasse_Minkowski0 (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
hV : Module.rank ℚ V = 0
⊢ ∀ (F : QuadraticForm ℚ V), Hasse_Minkowski F
Tactic:
intro F
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

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]
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

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
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

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
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

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
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

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]
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

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]
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

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
State after:
no goals

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
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

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
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

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]
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))

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
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)

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
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)

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]
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)

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
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

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]
State after:
no goals