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

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