Commit 2023-06-26 14:00 440cc2bc

View on Github →

feat: port NumberTheory.Zsqrtd.QuadraticReciprocity (#5485)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/Zsqrtd/QuadraticReciprocity.lean

added theorem GaussianInt.mod_four_eq_three_of_nat_prime_of_prime

added theorem GaussianInt.prime_iff_mod_four_eq_three_of_nat_prime

added theorem GaussianInt.prime_of_nat_prime_of_mod_four_eq_three