Commit 2023-06-26 12:34 faea138e

View on Github →

feat: port NumberTheory.LegendreSymbol.QuadraticChar.GaussSum (#5481)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/GaussSum.lean

added theorem FiniteField.isSquare_neg_two_iff

added theorem FiniteField.isSquare_odd_prime_iff

added theorem FiniteField.isSquare_two_iff

added theorem quadraticChar_card_card

added theorem quadraticChar_neg_two

added theorem quadraticChar_odd_prime

added theorem quadraticChar_two