chore(linear_algebra/quadratic_form): add polar_self, polar_zero_left…

…, and polar_zero_right simp lemmas (#6003)

This also reorders the existing lemmas to keep the polar ones separate from the non-polar ones

src/linear_algebra/quadratic_form.lean

@@ -102,6 +102,24 @@ instance : has_coe_to_fun (quadratic_form R M) :=
 /-- The `simp` normal form for a quadratic form is `coe_fn`, not `to_fun`. -/
 @[simp] lemma to_fun_eq_apply : Q.to_fun = ⇑ Q := rfl
 
+lemma map_smul (a : R) (x : M) : Q (a • x) = a * a * Q x := Q.to_fun_smul a x
+
+lemma map_add_self (x : M) : Q (x + x) = 4 * Q x :=
+by { rw [←one_smul R x, ←add_smul, map_smul], norm_num }
+
+@[simp] lemma map_zero : Q 0 = 0 :=
+by rw [←@zero_smul R _ _ _ _ (0 : M), map_smul, zero_mul, zero_mul]
+
+@[simp] lemma map_neg (x : M) : Q (-x) = Q x :=
+by rw [←@neg_one_smul R _ _ _ _ x, map_smul, neg_one_mul, neg_neg, one_mul]
+
+lemma map_sub (x y : M) : Q (x - y) = Q (y - x) :=
+by rw [←neg_sub, map_neg]
+
+@[simp]
+lemma polar_zero_left (y : M) : polar Q 0 y = 0 :=
+by simp [polar]
+
 @[simp]
 lemma polar_add_left (x x' y : M) :
   polar Q (x + x') y = polar Q x y + polar Q x' y :=
@@ -122,6 +140,10 @@ lemma polar_sub_left (x x' y : M) :
   polar Q (x - x') y = polar Q x y - polar Q x' y :=
 by rw [sub_eq_add_neg, sub_eq_add_neg, polar_add_left, polar_neg_left]
 
+@[simp]
+lemma polar_zero_right (y : M) : polar Q y 0 = 0 :=
+by simp [polar]
+
 @[simp]
 lemma polar_add_right (x y y' : M) :
   polar Q x (y + y') = polar Q x y + polar Q x y' :=
@@ -142,19 +164,12 @@ lemma polar_sub_right (x y y' : M) :
   polar Q x (y - y') = polar Q x y - polar Q x y' :=
 by rw [sub_eq_add_neg, sub_eq_add_neg, polar_add_right, polar_neg_right]
 
-lemma map_smul (a : R) (x : M) : Q (a • x) = a * a * Q x := Q.to_fun_smul a x
-
-lemma map_add_self (x : M) : Q (x + x) = 4 * Q x :=
-by { rw [←one_smul R x, ←add_smul, map_smul], norm_num }
-
-@[simp] lemma map_zero : Q 0 = 0 :=
-by rw [←@zero_smul R _ _ _ _ (0 : M), map_smul, zero_mul, zero_mul]
-
-@[simp] lemma map_neg (x : M) : Q (-x) = Q x :=
-by rw [←@neg_one_smul R _ _ _ _ x, map_smul, neg_one_mul, neg_neg, one_mul]
-
-lemma map_sub (x y : M) : Q (x - y) = Q (y - x) :=
-by rw [←neg_sub, map_neg]
+@[simp]
+lemma polar_self (x : M) : polar Q x x = 2 * Q x :=
+begin
+  rw [polar, map_add_self, sub_sub, sub_eq_iff_eq_add, ←two_mul, ←two_mul, ←mul_assoc],
+  norm_num
+end
 
 variable {Q' : quadratic_form R M}
 @[ext] lemma ext (H : ∀ (x : M), Q x = Q' x) : Q = Q' :=