Skip to content

Instantly share code, notes, and snippets.

@jorendorff

jorendorff/euler_four_square_identity.lean

Created July 25, 2020 23:18
Show Gist options
  • Save jorendorff/983f32339785b178b864eb82acc2299c to your computer and use it in GitHub Desktop.
Save jorendorff/983f32339785b178b864eb82acc2299c to your computer and use it in GitHub Desktop.
Download ZIP
Raw
euler_four_square_identity.lean
import algebra.ring
import tactic
def sqr {α} [ring α] (a : α) := a * a
theorem euler_four_square_identity {α} [comm_ring α]
: ∀ a₁ a₂ a₃ a₄ b₁ b₂ b₃ b₄ : α, ∃ c₁ c₂ c₃ c₄ : α,
(sqr a₁ + sqr a₂ + sqr a₃ + sqr a₄) * (sqr b₁ + sqr b₂ + sqr b₃ + sqr b₄)
= (sqr c₁ + sqr c₂ + sqr c₃ + sqr c₄)
:= by {
intros,
use a₁ * b₁ - a₂ * b₂ - a₃ * b₃ - a₄ * b₄,
use a₁ * b₂ + a₂ * b₁ + a₃ * b₄ - a₄ * b₃,
use a₁ * b₃ - a₂ * b₄ + a₃ * b₁ + a₄ * b₂,
use a₁ * b₄ + a₂ * b₃ - a₃ * b₂ + a₄ * b₁,
dsimp [sqr],
ring -- Quite Easily Done, as an algebra teacher of mine used to say
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment