feat(algebra/group_power/identities): named ring identities (#4390)

This PR adds a new file containing some "named" ring identities provable by `ring`.

Author: bryangingechen

src/algebra/group_power/identities.lean

@@ -0,0 +1,71 @@
+/-
+Copyright (c) 2020 Bryan Gin-ge Chen. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bryan Gin-ge Chen, Kevin Lacker
+-/
+import tactic.ring
+/-!
+# Identities
+
+This file contains some "named" commutative ring identities.
+-/
+
+variables {R : Type*} [comm_ring R]
+{a b x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈ y₁ y₂ y₃ y₄ y₅ y₆ y₇ y₈ n : R}
+
+/--
+Brahmagupta-Fibonacci identity or Diophantus identity, see
+<https://en.wikipedia.org/wiki/Brahmagupta%E2%80%93Fibonacci_identity>.
+
+This sign choice here corresponds to the signs obtained by multiplying two complex numbers.
+-/
+theorem pow_two_add_pow_two_mul_pow_two_add_pow_two :
+  (x₁^2 + x₂^2) * (y₁^2 + y₂^2) = (x₁*y₁ - x₂*y₂)^2 + (x₁*y₂ + x₂*y₁)^2 :=
+by ring
+
+/--
+Brahmagupta's identity, see <https://en.wikipedia.org/wiki/Brahmagupta%27s_identity>
+-/
+theorem pow_two_add_mul_pow_two_mul_pow_two_add_mul_pow_two :
+  (x₁^2 + n*x₂^2) * (y₁^2 + n*y₂^2) = (x₁*y₁ - n*x₂*y₂)^2 + n*(x₁*y₂ + x₂*y₁)^2 :=
+by ring
+
+/--
+Sophie Germain's identity, see <https://www.cut-the-knot.org/blue/SophieGermainIdentity.shtml>.
+-/
+theorem pow_four_add_four_mul_pow_four : a^4 + 4*b^4 = ((a - b)^2 + b^2) * ((a + b)^2 + b^2) :=
+by ring
+
+/--
+Sophie Germain's identity, see <https://www.cut-the-knot.org/blue/SophieGermainIdentity.shtml>.
+-/
+theorem pow_four_add_four_mul_pow_four' :
+  a^4 + 4*b^4 = (a^2 - 2*a*b + 2*b^2) * (a^2 + 2*a*b + 2*b^2) :=
+by ring
+
+/--
+Euler's four-square identity, see <https://en.wikipedia.org/wiki/Euler%27s_four-square_identity>.
+
+This sign choice here corresponds to the signs obtained by multiplying two quaternions.
+-/
+theorem sum_four_sq_mul_sum_four_sq : (x₁^2 + x₂^2 + x₃^2 + x₄^2) * (y₁^2 + y₂^2 + y₃^2 + y₄^2) =
+  (x₁*y₁ - x₂*y₂ - x₃*y₃ - x₄*y₄)^2 + (x₁*y₂ + x₂*y₁ + x₃*y₄ - x₄*y₃)^2 +
+  (x₁*y₃ - x₂*y₄ + x₃*y₁ + x₄*y₂)^2 + (x₁*y₄ + x₂*y₃ - x₃*y₂ + x₄*y₁)^2 :=
+by ring
+
+/--
+Degen's eight squares identity, see <https://en.wikipedia.org/wiki/Degen%27s_eight-square_identity>.
+
+This sign choice here corresponds to the signs obtained by multiplying two octonions.
+-/
+theorem sum_eight_sq_mul_sum_eight_sq : (x₁^2 + x₂^2 + x₃^2 + x₄^2 + x₅^2 + x₆^2 + x₇^2 + x₈^2) *
+  (y₁^2 + y₂^2 + y₃^2 + y₄^2 + y₅^2 + y₆^2 + y₇^2 + y₈^2) =
+  (x₁*y₁ - x₂*y₂ - x₃*y₃ - x₄*y₄ - x₅*y₅ - x₆*y₆ - x₇*y₇ - x₈*y₈)^2 +
+  (x₁*y₂ + x₂*y₁ + x₃*y₄ - x₄*y₃ + x₅*y₆ - x₆*y₅ - x₇*y₈ + x₈*y₇)^2 +
+  (x₁*y₃ - x₂*y₄ + x₃*y₁ + x₄*y₂ + x₅*y₇ + x₆*y₈ - x₇*y₅ - x₈*y₆)^2 +
+  (x₁*y₄ + x₂*y₃ - x₃*y₂ + x₄*y₁ + x₅*y₈ - x₆*y₇ + x₇*y₆ - x₈*y₅)^2 +
+  (x₁*y₅ - x₂*y₆ - x₃*y₇ - x₄*y₈ + x₅*y₁ + x₆*y₂ + x₇*y₃ + x₈*y₄)^2 +
+  (x₁*y₆ + x₂*y₅ - x₃*y₈ + x₄*y₇ - x₅*y₂ + x₆*y₁ - x₇*y₄ + x₈*y₃)^2 +
+  (x₁*y₇ + x₂*y₈ + x₃*y₅ - x₄*y₆ - x₅*y₃ + x₆*y₄ + x₇*y₁ - x₈*y₂)^2 +
+  (x₁*y₈ - x₂*y₇ + x₃*y₆ + x₄*y₅ - x₅*y₄ - x₆*y₃ + x₇*y₂ + x₈*y₁)^2 :=
+by ring

src/number_theory/sum_four_squares.lean

@@ -12,6 +12,7 @@ a proof that every natural number is the sum of four square numbers.
 
 The proof used is close to Lagrange's original proof.
 -/
+import algebra.group_power.identities
 import data.zmod.basic
 import field_theory.finite.basic
 import data.int.parity
@@ -201,14 +202,13 @@ have n / min_fac n < n := factors_lemma,
 let ⟨a, b, c, d, h₁⟩ := show ∃ a b c d : ℤ, a^2 + b^2 + c^2 + d^2 = min_fac n,
   by exactI prime_sum_four_squares (min_fac (k+2)) in
 let ⟨w, x, y, z, h₂⟩ := sum_four_squares (n / min_fac n) in
-⟨(a * x - b * w - c * z + d * y).nat_abs,
- (a * y + b * z - c * w - d * x).nat_abs,
- (a * z - b * y + c * x - d * w).nat_abs,
- (a * w + b * x + c * y + d * z).nat_abs,
+⟨(a * w - b * x - c * y - d * z).nat_abs,
+ (a * x + b * w + c * z - d * y).nat_abs,
+ (a * y - b * z + c * w + d * x).nat_abs,
+ (a * z + b * y - c * x + d * w).nat_abs,
   begin
     rw [← int.coe_nat_inj', ← nat.mul_div_cancel' (min_fac_dvd (k+2)), int.coe_nat_mul, ← h₁, ← h₂],
-    simp,
-    ring
+    simp [sum_four_sq_mul_sum_four_sq],
   end⟩
 
 end nat