Commit 2024-05-31 13:35 2171e8de

View on Github →

feat: add API for additive characters (#13389) This adds some API lemmas for additive characters.

Name change: AddChar.primitiveCharFiniteField to AddChar.FiniteField.primitiveChar We also remove a porting note (AddChar.PrimitiveAddChar can be a structure again) and fix a typo in a lemma name from another recent PR.

Estimated changes

Modified Mathlib/Algebra/Group/AddChar.lean

added theorem AddChar.val_isUnit

Modified Mathlib/NumberTheory/LegendreSymbol/AddCharacter.lean

added theorem AddChar.FiniteField.primitiveChar_to_Complex_isPrimitive

added theorem AddChar.IsPrimitive.compMulHom_of_isPrimitive

deleted theorem AddChar.PrimitiveAddChar.prim

added structure AddChar.PrimitiveAddChar

deleted def AddChar.PrimitiveAddChar

added theorem AddChar.starComp_apply

added theorem AddChar.starComp_eq_inv

added theorem AddChar.val_mem_rootsOfUnity

Modified Mathlib/NumberTheory/LegendreSymbol/GaussSum.lean

Modified Mathlib/RingTheory/RootsOfUnity/Complex.lean

deleted theorem Complex.norm_eq_one_of_mem_rootOfUnity

added theorem Complex.norm_eq_one_of_mem_rootsOfUnity