Commit 2024-07-31 20:15 c4b7ae4b

View on Github →

feat(LegendreSymbol/AddCharacter): std add char of ZMod N is primitive (#14495) The standard additive character of ZMod N is a primitive character.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Fourier/ZMod.lean

Modified Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean

added theorem AddCircle.toCircle_zero

deleted theorem ZMod.stdAddChar_apply

deleted theorem ZMod.stdAddChar_coe

deleted theorem ZMod.toCircle_apply

deleted theorem ZMod.toCircle_intCast

deleted theorem ZMod.toCircle_natCast

Created Mathlib/Analysis/SpecialFunctions/Complex/CircleAddChar.lean

added theorem ZMod.injective_stdAddChar

added theorem ZMod.injective_toCircle

added theorem ZMod.isPrimitive_stdAddChar

added theorem ZMod.stdAddChar_apply

added theorem ZMod.stdAddChar_coe

added theorem ZMod.toCircle_apply

added theorem ZMod.toCircle_intCast

added theorem ZMod.toCircle_natCast