sq_add_mul_sq_mul_sq_add_mul_sq — Mathlib

English

Product of sums of eight squares equals a sum of eight squares with a specific nested sign pattern, related to octonions.

Русский

Произведение сумм восьми квадратов равно сумме восьми квадратов с конкретной схемой знаков, связанной с октониками.

LaTeX

$$The long explicit equality of eight-square identity as stated in the theorem.$$

Lean4

/-- Brahmagupta's identity, see <https://en.wikipedia.org/wiki/Brahmagupta%27s_identity>
-/
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 := by ring

Похожие утверждения