Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
/-
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
:=

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₁) ^ 2

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
:=

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₁) ^ 2

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
) :=

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)

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
) :=

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)

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
:=

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₁) ^ 2

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
:=

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₁) ^ 2

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