no goals
S : Type ?u.139031
R : Type u_1
R₁ : Type ?u.139037
M : Type u_2
inst✝³ : Ring R
inst✝² : CommRing R₁
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : M
⊢ ↑Q (-x) = ↑Q x
rw [← @neg_one_smul R _ _ _ _ x, map_smul, neg_one_mul, neg_neg, one_mul]