no goals
S : Type ?u.126220
R : Type u_1
R₁ : Type ?u.126226
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ ↑Q 0 = 0
rw [← @zero_smul R _ _ _ _ (0 : M), map_smul, zero_mul, zero_mul]