Commit 2023-06-26 14:58 0b5fe726

View on Github →

feat: port NumberTheory.SumTwoSquares (#5487)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/SumTwoSquares.lean

added theorem Nat.Prime.mod_four_ne_three_of_dvd_isSquare_neg_one

added theorem Nat.Prime.sq_add_sq

added theorem Nat.eq_sq_add_sq_iff

added theorem Nat.eq_sq_add_sq_iff_eq_sq_mul

added theorem Nat.eq_sq_add_sq_of_isSquare_mod_neg_one

added theorem Nat.sq_add_sq_mul

added theorem ZMod.isSquare_neg_one_iff'

added theorem ZMod.isSquare_neg_one_iff

added theorem ZMod.isSquare_neg_one_mul

added theorem ZMod.isSquare_neg_one_of_dvd

added theorem ZMod.isSquare_neg_one_of_eq_sq_add_sq_of_coprime

added theorem ZMod.isSquare_neg_one_of_eq_sq_add_sq_of_isCoprime

added theorem sq_add_sq_mul