Theorem: baseChange_of_degenerate (AntLorentz/BaseChange.lean)

State before:
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 (↑associated (baseChange A Q))
Tactic:
simp only [baseChange_associated]
State after:
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))

State before:
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))
Tactic:
exact BilinForm.baseChange_of_degenerate _ hQ
State after:
no goals