exact BilinForm.baseChange_of_degenerate _ hQ
M k A : Type
inst✝¹² : Field k
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module k M
inst✝⁹ : CommRing A
inst✝⁸ : Algebra k A
inst✝⁷ : Module A M
inst✝⁶ : IsScalarTower k A M
inst✝⁵ : StrongRankCondition A
inst✝⁴ : Module.Free k M
inst✝³ : Module.Free A M
inst✝² : Module.Free k A
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q : QuadraticForm k M
hQ : ¬BilinForm.Nondegenerate (↑associated Q)
⊢ ¬BilinForm.Nondegenerate (BilinForm.baseChange A (↑associated Q))
no goals