Theorem: QuadraticForm.HasseMinkowski_of_degenerate (AntLorentz/HasseMinkowski.lean)

State before:
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.104463
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q : QuadraticForm ℚ V
hQ : ¬BilinForm.Nondegenerate (↑associated Q)
⊢ HasseMinkowski Q
Tactic:
have degenQ := Q.nondegenerate_of_anisotropic.mt hQ
State after:
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.104463
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q : QuadraticForm ℚ V
hQ : ¬BilinForm.Nondegenerate (↑associated Q)
degenQ : ¬Anisotropic Q
⊢ HasseMinkowski Q

State before:
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.104463
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q : QuadraticForm ℚ V
hQ : ¬BilinForm.Nondegenerate (↑associated Q)
degenQ : ¬Anisotropic Q
⊢ HasseMinkowski Q
Tactic:
have degenR := (nondegenerate_of_anisotropic _).mt (baseChange_of_degenerate (A := ℝ) _ hQ)
State after:
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.104463
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q : QuadraticForm ℚ V
hQ : ¬BilinForm.Nondegenerate (↑associated Q)
degenQ : ¬Anisotropic Q
degenR : ¬Anisotropic (baseChange ℝ Q)
⊢ HasseMinkowski Q

State before:
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.104463
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q : QuadraticForm ℚ V
hQ : ¬BilinForm.Nondegenerate (↑associated Q)
degenQ : ¬Anisotropic Q
degenR : ¬Anisotropic (baseChange ℝ Q)
⊢ HasseMinkowski Q
Tactic:
simp only [HasseMinkowski, Isotropic, degenQ, not_false_eq_true,
  EverywhereLocallyIsotropic, degenR, and_true, true_iff]
State after:
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.104463
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q : QuadraticForm ℚ V
hQ : ¬BilinForm.Nondegenerate (↑associated Q)
degenQ : ¬Anisotropic Q
degenR : ¬Anisotropic (baseChange ℝ Q)
⊢ ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ¬Anisotropic (baseChange ℚ_[p] Q)

State before:
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.104463
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q : QuadraticForm ℚ V
hQ : ¬BilinForm.Nondegenerate (↑associated Q)
degenQ : ¬Anisotropic Q
degenR : ¬Anisotropic (baseChange ℝ Q)
⊢ ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ¬Anisotropic (baseChange ℚ_[p] Q)
Tactic:
intro p hp
State after:
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.104463
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q : QuadraticForm ℚ V
hQ : ¬BilinForm.Nondegenerate (↑associated Q)
degenQ : ¬Anisotropic Q
degenR : ¬Anisotropic (baseChange ℝ Q)
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ¬Anisotropic (baseChange ℚ_[p] Q)

State before:
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.104463
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
Q : QuadraticForm ℚ V
hQ : ¬BilinForm.Nondegenerate (↑associated Q)
degenQ : ¬Anisotropic Q
degenR : ¬Anisotropic (baseChange ℝ Q)
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ¬Anisotropic (baseChange ℚ_[p] Q)
Tactic:
exact (nondegenerate_of_anisotropic (Q.baseChange ℚ_[p])).mt (baseChange_of_degenerate (A := ℚ_[p]) _ hQ)
State after:
no goals