Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-10-29 22:34 ca900815

View on Github →

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

Estimated changes

Modified src/algebra/big_operators.lean

added theorem finset.prod_eq_multiset_prod

Modified src/data/int/basic.lean

added theorem is_ring_hom.map_int_cast

added theorem ring_hom.map_int_cast

Modified src/data/int/parity.lean

added theorem int.even_neg

Modified src/data/nat/cast.lean

added theorem is_semiring_hom.map_nat_cast

added theorem ring_hom.map_nat_cast

Modified src/data/zmod/quadratic_reciprocity.lean

Modified src/field_theory/finite.lean

added theorem char_p.sum_two_squares

added theorem zmodp.sum_two_squares

Created src/number_theory/sum_four_squares.lean

added theorem int.exists_sum_two_squares_add_one_eq_k

added theorem int.sum_two_squares_of_two_mul_sum_two_squares

added theorem nat.sum_four_squares