Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-11-05 15:37 986e58ca

View on Github →

refactor(sum_two_square): extract lemmas about primes in Z[i] (#1643)

refactor(sum_two_square): extract lemmas about primes in Z[i]
forgot to save
docztring
module docstrings

Estimated changes

Modified src/data/zsqrtd/gaussian_int.lean

added theorem gaussian_int.mod_four_eq_three_of_nat_prime_of_prime

added theorem gaussian_int.prime_iff_mod_four_eq_three_of_nat_prime

added theorem gaussian_int.prime_of_nat_prime_of_mod_four_eq_three

added theorem gaussian_int.sum_two_squares_of_nat_prime_of_not_irreducible

Modified src/number_theory/sum_two_squares.lean