Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-02 17:42 9c9aee45

View on Github →

finish proof of sum two squares

Estimated changes

Modified src/data/nat/prime.lean

added theorem nat.prime.mul_eq_prime_pow_two

Modified src/data/zmod/quadratic_reciprocity.lean

Modified src/number_theory/sum_two_squares.lean

added theorem gaussian_int.norm_eq_one_iff

added theorem gaussian_int.norm_le_norm_mul_left

added theorem gaussian_int.norm_nat_cast

added theorem gaussian_int.norm_one

added theorem gaussian_int.norm_zero

added theorem sum_two_squares