Commit 2023-06-26 10:09 5775c852

View on Github →

feat: port NumberTheory.LegendreSymbol.GaussSum (#5419) This PR incorporates also the changes to NumberTheory.LegendreSymbol.MulCharacter discussed here

Estimated changes

Modified Mathlib.lean

Modified Mathlib/NumberTheory/LegendreSymbol/Basic.lean

Created Mathlib/NumberTheory/LegendreSymbol/GaussSum.lean

added theorem Char.card_pow_card

added theorem Char.card_pow_char_pow

added theorem FiniteField.two_pow_card

added theorem MulChar.IsQuadratic.gaussSum_frob_iter

added def gaussSum

added theorem gaussSum_frob

added theorem gaussSum_mulShift

added theorem gaussSum_mul_gaussSum_eq_card

added theorem gaussSum_sq

Modified Mathlib/NumberTheory/LegendreSymbol/MulCharacter.lean

deleted theorem MulChar.coe_coe

deleted theorem MulChar.toFun_eq_coe

Modified Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/Basic.lean

Modified Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean