mathlib

ca900815 - feat(number_theory/sum_four_squares): every natural number is the sum of four square numbers (#1560)

feat(number_theory/sum_four_squares): every natural number is the sum of four square numbers (#1560) * feat(number_theory/sum_four_squares): every natural number is the sum of four square numbers * Johan's suggestions * some better parity proofs * fix silly lemmas in finite_fields * generalize a lemma * fix build * Update src/number_theory/sum_four_squares.lean * add docs in correct style