Lagrange's four square theorem #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
The main result in this file is
a proof that every natural number is the sum of four square numbers.
Implementation Notes #
The proof used is close to Lagrange's original proof.