Commit 2023-06-04 07:30 eb95d896

View on Github →

feat: port NumberTheory.SumFourSquares (#4604)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Nat/Order/Lemmas.lean

added theorem Nat.mul_div_eq_iff_dvd

added theorem Nat.mul_div_lt_iff_not_dvd

Modified Mathlib/Data/Nat/Parity.lean

added theorem Odd.not_two_dvd_nat

Modified Mathlib/FieldTheory/Finite/Basic.lean

added theorem Nat.sq_add_sq_modEq

added theorem Nat.sq_add_sq_zmodEq

Created Mathlib/NumberTheory/SumFourSquares.lean

added theorem Int.exists_sq_add_sq_add_one_eq_k

added theorem Int.exists_sq_add_sq_add_one_eq_mul

added theorem Int.lt_of_sum_four_squares_eq_mul

added theorem Int.sq_add_sq_of_two_mul_sq_add_sq

added theorem Nat.euler_four_squares

added theorem Nat.sum_four_squares

added theorem euler_four_squares