S : Type ?u.122615
R : Type u_1
R₁ : Type ?u.122621
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
Q : QuadraticForm R M
x : M
⊢ (1 + 1) * (1 + 1) * ↑Q x = 4 * ↑Q (1 • x)
S : Type ?u.122615
R : Type u_1
R₁ : Type ?u.122621
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
Q : QuadraticForm R M
x : M
⊢ ↑Q (x + x) = 4 * ↑Q x
rw [← one_smul R x, ← add_smul, map_smul]
no goals
S : Type ?u.122615
R : Type u_1
R₁ : Type ?u.122621
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
Q : QuadraticForm R M
x : M
⊢ (1 + 1) * (1 + 1) * ↑Q x = 4 * ↑Q (1 • x)
norm_num