/-
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

! This file was ported from Lean 3 source module algebra.group_power.identities
! leanprover-community/mathlib commit c4658a649d216f57e99621708b09dcb3dcccbd23
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Tactic.Ring

/-!
# Identities

This file contains some "named" commutative ring identities.
-/


variable {
R: Type ?u.11796
R : 
Type _: Type (?u.11796+1)
Type _} [
CommRing: Type ?u.5 → Type ?u.5
CommRing 
R: Type ?u.46
R] {
a: R
a 
b: R
b 
x₁: R
x₁ 
x₂: R
x₂ 
x₃: R
x₃ 
x₄: R
x₄ 
x₅: R
x₅ 
x₆: R
x₆ 
x₇: R
x₇ 
x₈: R
x₈ 
y₁: R
y₁ 
y₂: R
y₂ 
y₃: R
y₃ 
y₄: R
y₄ 
y₅: R
y₅ 
y₆: R
y₆ 
y₇: R
y₇ 
y₈: R
y₈ 
n: R
n : 
R: Type ?u.46
R}

/-- Brahmagupta-Fibonacci identity or Diophantus identity, see
.

This sign choice here corresponds to the signs obtained by multiplying two complex numbers.
-/
theorem 
sq_add_sq_mul_sq_add_sq: (x₁ ^ 2 + x₂ ^ 2) * (y₁ ^ 2 + y₂ ^ 2) = (x₁ * y₁ - x₂ * y₂) ^ 2 + (x₁ * y₂ + x₂ * y₁) ^ 2
sq_add_sq_mul_sq_add_sq :
    (
x₁: R
x₁ ^ 
2: ?m.101
2 + 
x₂: R
x₂ ^ 
2: ?m.114
2) * (
y₁: R
y₁ ^ 
2: ?m.130
2 + 
y₂: R
y₂ ^ 
2: ?m.143
2) = (
x₁: R
x₁ * 
y₁: R
y₁ - 
x₂: R
x₂ * 
y₂: R
y₂) ^ 
2: ?m.184
2 + (
x₁: R
x₁ * 
y₂: R
y₂ + 
x₂: R
x₂ * 
y₁: R
y₁) ^ 
2: ?m.206
2 := by
Goals accomplished! 🐙
  
R: Type u_1

inst✝: CommRing R

a, b, x₁, x₂, x₃, x₄, x₅, x₆, x₇, x₈, y₁, y₂, y₃, y₄, y₅, y₆, y₇, y₈, n: R

(x₁ ^ 2 + x₂ ^ 2) * (y₁ ^ 2 + y₂ ^ 2) = (x₁ * y₁ - x₂ * y₂) ^ 2 + (x₁ * y₂ + x₂ * y₁) ^ 2ring
Goals accomplished! 🐙
#align sq_add_sq_mul_sq_add_sq 
sq_add_sq_mul_sq_add_sq: ∀ {R : Type u_1} [inst : CommRing R] {x₁ x₂ y₁ y₂ : R},
  (x₁ ^ 2 + x₂ ^ 2) * (y₁ ^ 2 + y₂ ^ 2) = (x₁ * y₁ - x₂ * y₂) ^ 2 + (x₁ * y₂ + x₂ * y₁) ^ 2
sq_add_sq_mul_sq_add_sq

/-- Brahmagupta's identity, see 
-/
theorem 
sq_add_mul_sq_mul_sq_add_mul_sq: (x₁ ^ 2 + n * x₂ ^ 2) * (y₁ ^ 2 + n * y₂ ^ 2) = (x₁ * y₁ - n * x₂ * y₂) ^ 2 + n * (x₁ * y₂ + x₂ * y₁) ^ 2
sq_add_mul_sq_mul_sq_add_mul_sq :
    (
x₁: R
x₁ ^ 
2: ?m.3770
2 + 
n: R
n * 
x₂: R
x₂ ^ 
2: ?m.3786
2) * (
y₁: R
y₁ ^ 
2: ?m.3802
2 + 
n: R
n * 
y₂: R
y₂ ^ 
2: ?m.3818
2) =
    (
x₁: R
x₁ * 
y₁: R
y₁ - 
n: R
n * 
x₂: R
x₂ * 
y₂: R
y₂) ^ 
2: ?m.3862
2 + 
n: R
n * (
x₁: R
x₁ * 
y₂: R
y₂ + 
x₂: R
x₂ * 
y₁: R
y₁) ^ 
2: ?m.3887
2 := by
Goals accomplished! 🐙
  
R: Type u_1

inst✝: CommRing R

a, b, x₁, x₂, x₃, x₄, x₅, x₆, x₇, x₈, y₁, y₂, y₃, y₄, y₅, y₆, y₇, y₈, n: R

(x₁ ^ 2 + n * x₂ ^ 2) * (y₁ ^ 2 + n * y₂ ^ 2) = (x₁ * y₁ - n * x₂ * y₂) ^ 2 + n * (x₁ * y₂ + x₂ * y₁) ^ 2ring
Goals accomplished! 🐙
#align sq_add_mul_sq_mul_sq_add_mul_sq 
sq_add_mul_sq_mul_sq_add_mul_sq: ∀ {R : Type u_1} [inst : CommRing R] {x₁ x₂ y₁ y₂ n : R},
  (x₁ ^ 2 + n * x₂ ^ 2) * (y₁ ^ 2 + n * y₂ ^ 2) = (x₁ * y₁ - n * x₂ * y₂) ^ 2 + n * (x₁ * y₂ + x₂ * y₁) ^ 2
sq_add_mul_sq_mul_sq_add_mul_sq

/-- Sophie Germain's identity, see .
-/
theorem 
pow_four_add_four_mul_pow_four: ∀ {R : Type u_1} [inst : CommRing R] {a b : R}, a ^ 4 + 4 * b ^ 4 = ((a - b) ^ 2 + b ^ 2) * ((a + b) ^ 2 + b ^ 2)
pow_four_add_four_mul_pow_four :
    
a: R
a ^ 
4: ?m.7994
4 + 
4: ?m.8007
4 * 
b: R
b ^ 
4: ?m.8020
4 = ((
a: R
a - 
b: R
b) ^ 
2: ?m.8054
2 + 
b: R
b ^ 
2: ?m.8067
2) * ((
a: R
a + 
b: R
b) ^ 
2: ?m.8086
2 + 
b: R
b ^ 
2: ?m.8099
2) := by
Goals accomplished! 🐙
  
R: Type u_1

inst✝: CommRing R

a, b, x₁, x₂, x₃, x₄, x₅, x₆, x₇, x₈, y₁, y₂, y₃, y₄, y₅, y₆, y₇, y₈, n: R

a ^ 4 + 4 * b ^ 4 = ((a - b) ^ 2 + b ^ 2) * ((a + b) ^ 2 + b ^ 2)ring
Goals accomplished! 🐙
#align pow_four_add_four_mul_pow_four 
pow_four_add_four_mul_pow_four: ∀ {R : Type u_1} [inst : CommRing R] {a b : R}, a ^ 4 + 4 * b ^ 4 = ((a - b) ^ 2 + b ^ 2) * ((a + b) ^ 2 + b ^ 2)
pow_four_add_four_mul_pow_four

/-- Sophie Germain's identity, see .
-/
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)
pow_four_add_four_mul_pow_four' :
    
a: R
a ^ 
4: ?m.11848
4 + 
4: ?m.11861
4 * 
b: R
b ^ 
4: ?m.11874
4 = (
a: R
a ^ 
2: ?m.11908
2 - 
2: ?m.11924
2 * 
a: R
a * 
b: R
b + 
2: ?m.11937
2 * 
b: R
b ^ 
2: ?m.11950
2) * (
a: R
a ^ 
2: ?m.11969
2 + 
2: ?m.11985
2 * 
a: R
a * 
b: R
b + 
2: ?m.11998
2 * 
b: R
b ^ 
2: ?m.12011
2) := by
Goals accomplished! 🐙
  
R: Type u_1

inst✝: CommRing R

a, b, x₁, x₂, x₃, x₄, x₅, x₆, x₇, x₈, y₁, y₂, y₃, y₄, y₅, y₆, y₇, y₈, n: R

a ^ 4 + 4 * b ^ 4 = (a ^ 2 - 2 * a * b + 2 * b ^ 2) * (a ^ 2 + 2 * a * b + 2 * b ^ 2)ring
Goals accomplished! 🐙
#align pow_four_add_four_mul_pow_four' 
pow_four_add_four_mul_pow_four': ∀ {R : Type u_1} [inst : CommRing R] {a b : R},
  a ^ 4 + 4 * b ^ 4 = (a ^ 2 - 2 * a * b + 2 * b ^ 2) * (a ^ 2 + 2 * a * b + 2 * b ^ 2)
pow_four_add_four_mul_pow_four'

/-- Euler's four-square identity, see .

This sign choice here corresponds to the signs obtained by multiplying two quaternions.
-/
theorem 
sum_four_sq_mul_sum_four_sq: ∀ {R : Type u_1} [inst : CommRing R] {x₁ x₂ x₃ x₄ y₁ y₂ y₃ y₄ : R},
  (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
sum_four_sq_mul_sum_four_sq :
    (
x₁: R
x₁ ^ 
2: ?m.16764
2 + 
x₂: R
x₂ ^ 
2: ?m.16777
2 + 
x₃: R
x₃ ^ 
2: ?m.16790
2 + 
x₄: R
x₄ ^ 
2: ?m.16803
2) * (
y₁: R
y₁ ^ 
2: ?m.16825
2 + 
y₂: R
y₂ ^ 
2: ?m.16838
2 + 
y₃: R
y₃ ^ 
2: ?m.16851
2 + 
y₄: R
y₄ ^ 
2: ?m.16864
2) =
      (
x₁: R
x₁ * 
y₁: R
y₁ - 
x₂: R
x₂ * 
y₂: R
y₂ - 
x₃: R
x₃ * 
y₃: R
y₃ - 
x₄: R
x₄ * 
y₄: R
y₄) ^ 
2: ?m.16939
2 + (
x₁: R
x₁ * 
y₂: R
y₂ + 
x₂: R
x₂ * 
y₁: R
y₁ + 
x₃: R
x₃ * 
y₄: R
y₄ - 
x₄: R
x₄ * 
y₃: R
y₃) ^ 
2: ?m.16973
2 +
          (
x₁: R
x₁ * 
y₃: R
y₃ - 
x₂: R
x₂ * 
y₄: R
y₄ + 
x₃: R
x₃ * 
y₁: R
y₁ + 
x₄: R
x₄ * 
y₂: R
y₂) ^ 
2: ?m.17007
2 +
        (
x₁: R
x₁ * 
y₄: R
y₄ + 
x₂: R
x₂ * 
y₃: R
y₃ - 
x₃: R
x₃ * 
y₂: R
y₂ + 
x₄: R
x₄ * 
y₁: R
y₁) ^ 
2: ?m.17041
2 :=
  by
Goals accomplished! 🐙 
R: Type u_1

inst✝: CommRing R

a, b, x₁, x₂, x₃, x₄, x₅, x₆, x₇, x₈, y₁, y₂, y₃, y₄, y₅, y₆, y₇, y₈, n: R

(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₁) ^ 2ring
Goals accomplished! 🐙
#align sum_four_sq_mul_sum_four_sq 
sum_four_sq_mul_sum_four_sq: ∀ {R : Type u_1} [inst : CommRing R] {x₁ x₂ x₃ x₄ y₁ y₂ y₃ y₄ : R},
  (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
sum_four_sq_mul_sum_four_sq

/-- Degen's eight squares identity, see .

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
sum_eight_sq_mul_sum_eight_sq :
    (
x₁: R
x₁ ^ 
2: ?m.27384
2 + 
x₂: R
x₂ ^ 
2: ?m.27397
2 + 
x₃: R
x₃ ^ 
2: ?m.27410
2 + 
x₄: R
x₄ ^ 
2: ?m.27423
2 + 
x₅: R
x₅ ^ 
2: ?m.27436
2 + 
x₆: R
x₆ ^ 
2: ?m.27449
2 + 
x₇: R
x₇ ^ 
2: ?m.27462
2 + 
x₈: R
x₈ ^ 
2: ?m.27475
2) *
      (
y₁: R
y₁ ^ 
2: ?m.27509
2 + 
y₂: R
y₂ ^ 
2: ?m.27522
2 + 
y₃: R
y₃ ^ 
2: ?m.27535
2 + 
y₄: R
y₄ ^ 
2: ?m.27548
2 + 
y₅: R
y₅ ^ 
2: ?m.27561
2 + 
y₆: R
y₆ ^ 
2: ?m.27574
2 + 
y₇: R
y₇ ^ 
2: ?m.27587
2 + 
y₈: R
y₈ ^ 
2: ?m.27600
2) =
    (
x₁: R
x₁ * 
y₁: R
y₁ - 
x₂: R
x₂ * 
y₂: R
y₂ - 
x₃: R
x₃ * 
y₃: R
y₃ - 
x₄: R
x₄ * 
y₄: R
y₄ - 
x₅: R
x₅ * 
y₅: R
y₅ - 
x₆: R
x₆ * 
y₆: R
y₆ - 
x₇: R
x₇ * 
y₇: R
y₇ - 
x₈: R
x₈ * 
y₈: R
y₈) ^ 
2: ?m.27743
2 +
      (
x₁: R
x₁ * 
y₂: R
y₂ + 
x₂: R
x₂ * 
y₁: R
y₁ + 
x₃: R
x₃ * 
y₄: R
y₄ - 
x₄: R
x₄ * 
y₃: R
y₃ + 
x₅: R
x₅ * 
y₆: R
y₆ - 
x₆: R
x₆ * 
y₅: R
y₅ - 
x₇: R
x₇ * 
y₈: R
y₈ + 
x₈: R
x₈ * 
y₇: R
y₇) ^ 
2: ?m.27801
2 +
      (
x₁: R
x₁ * 
y₃: R
y₃ - 
x₂: R
x₂ * 
y₄: R
y₄ + 
x₃: R
x₃ * 
y₁: R
y₁ + 
x₄: R
x₄ * 
y₂: R
y₂ + 
x₅: R
x₅ * 
y₇: R
y₇ + 
x₆: R
x₆ * 
y₈: R
y₈ - 
x₇: R
x₇ * 
y₅: R
y₅ - 
x₈: R
x₈ * 
y₆: R
y₆) ^ 
2: ?m.27859
2 +
      (
x₁: R
x₁ * 
y₄: R
y₄ + 
x₂: R
x₂ * 
y₃: R
y₃ - 
x₃: R
x₃ * 
y₂: R
y₂ + 
x₄: R
x₄ * 
y₁: R
y₁ + 
x₅: R
x₅ * 
y₈: R
y₈ - 
x₆: R
x₆ * 
y₇: R
y₇ + 
x₇: R
x₇ * 
y₆: R
y₆ - 
x₈: R
x₈ * 
y₅: R
y₅) ^ 
2: ?m.27917
2 +
      (
x₁: R
x₁ * 
y₅: R
y₅ - 
x₂: R
x₂ * 
y₆: R
y₆ - 
x₃: R
x₃ * 
y₇: R
y₇ - 
x₄: R
x₄ * 
y₈: R
y₈ + 
x₅: R
x₅ * 
y₁: R
y₁ + 
x₆: R
x₆ * 
y₂: R
y₂ + 
x₇: R
x₇ * 
y₃: R
y₃ + 
x₈: R
x₈ * 
y₄: R
y₄) ^ 
2: ?m.27975
2 +
      (
x₁: R
x₁ * 
y₆: R
y₆ + 
x₂: R
x₂ * 
y₅: R
y₅ - 
x₃: R
x₃ * 
y₈: R
y₈ + 
x₄: R
x₄ * 
y₇: R
y₇ - 
x₅: R
x₅ * 
y₂: R
y₂ + 
x₆: R
x₆ * 
y₁: R
y₁ - 
x₇: R
x₇ * 
y₄: R
y₄ + 
x₈: R
x₈ * 
y₃: R
y₃) ^ 
2: ?m.28033
2 +
      (
x₁: R
x₁ * 
y₇: R
y₇ + 
x₂: R
x₂ * 
y₈: R
y₈ + 
x₃: R
x₃ * 
y₅: R
y₅ - 
x₄: R
x₄ * 
y₆: R
y₆ - 
x₅: R
x₅ * 
y₃: R
y₃ + 
x₆: R
x₆ * 
y₄: R
y₄ + 
x₇: R
x₇ * 
y₁: R
y₁ - 
x₈: R
x₈ * 
y₂: R
y₂) ^ 
2: ?m.28091
2 +
      (
x₁: R
x₁ * 
y₈: R
y₈ - 
x₂: R
x₂ * 
y₇: R
y₇ + 
x₃: R
x₃ * 
y₆: R
y₆ + 
x₄: R
x₄ * 
y₅: R
y₅ - 
x₅: R
x₅ * 
y₄: R
y₄ - 
x₆: R
x₆ * 
y₃: R
y₃ + 
x₇: R
x₇ * 
y₂: R
y₂ + 
x₈: R
x₈ * 
y₁: R
y₁) ^ 
2: ?m.28149
2 := by
Goals accomplished! 🐙
  
R: Type u_1

inst✝: CommRing R

a, b, x₁, x₂, x₃, x₄, x₅, x₆, x₇, x₈, y₁, y₂, y₃, y₄, y₅, y₆, y₇, y₈, n: R

(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₁) ^ 2ring
Goals accomplished! 🐙
#align sum_eight_sq_mul_sum_eight_sq 
sum_eight_sq_mul_sum_eight_sq: ∀ {R : Type u_1} [inst : CommRing R] {x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈ y₁ y₂ y₃ y₄ y₅ y₆ y₇ y₈ : R},
  (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
sum_eight_sq_mul_sum_eight_sq