S : Type ?u.174526
R : Type u_1
R₁ : Type ?u.174532
M : Type u_2
inst✝³ : Ring R
inst✝² : CommRing R₁
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : M
⊢ 4 * ↑Q x = 2 * 2 * ↑Q x
S : Type ?u.174526
R : Type u_1
R₁ : Type ?u.174532
M : Type u_2
inst✝³ : Ring R
inst✝² : CommRing R₁
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : M
⊢ polar (↑Q) x x = 2 * ↑Q x
rw [polar, map_add_self, sub_sub, sub_eq_iff_eq_add, ← two_mul, ← two_mul, ← mul_assoc]
no goals
S : Type ?u.174526
R : Type u_1
R₁ : Type ?u.174532
M : Type u_2
inst✝³ : Ring R
inst✝² : CommRing R₁
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : M
⊢ 4 * ↑Q x = 2 * 2 * ↑Q x
norm_num