Commit 2023-06-23 06:08 2c3a27aa

View on Github →

feat: port NumberTheory.LegendreSymbol.AddCharacter (#5397)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/FieldTheory/Finite/Trace.lean

deleted theorem FiniteField.trace_to_zMod_nondegenerate

added theorem FiniteField.trace_to_zmod_nondegenerate

Created Mathlib/NumberTheory/LegendreSymbol/AddCharacter.lean

added theorem AddChar.IsNontrivial.isPrimitive

added def AddChar.IsNontrivial

added theorem AddChar.IsPrimitive.zmod_char_eq_one_iff

added def AddChar.IsPrimitive

added theorem AddChar.PrimitiveAddChar.prim

added def AddChar.PrimitiveAddChar

added theorem AddChar.coe_to_fun_apply

added theorem AddChar.ext

added theorem AddChar.inv_apply

added theorem AddChar.inv_mulShift

added theorem AddChar.isNontrivial_iff_ne_trivial

added theorem AddChar.map_add_mul

added theorem AddChar.map_nsmul_pow

added theorem AddChar.map_zero_one

added theorem AddChar.map_zsmul_zpow

added def AddChar.mulShift

added theorem AddChar.mulShift_apply

added theorem AddChar.mulShift_mul

added theorem AddChar.mulShift_spec'

added theorem AddChar.mulShift_zero

added theorem AddChar.mul_apply

added theorem AddChar.one_apply

added theorem AddChar.pow_mulShift

added theorem AddChar.sum_eq_card_of_is_trivial

added theorem AddChar.sum_eq_zero_of_isNontrivial

added theorem AddChar.sum_mulShift

added def AddChar.toFun

added def AddChar.toMonoidHom

added theorem AddChar.to_mulShift_inj_of_isPrimitive

added def AddChar.zmodChar

added theorem AddChar.zmodChar_apply'

added theorem AddChar.zmodChar_apply

added theorem AddChar.zmodChar_primitive_of_primitive_root

added theorem AddChar.zmod_char_isNontrivial_iff

added theorem AddChar.zmod_char_primitive_of_eq_one_only_at_zero

added def AddChar