Commit 2024-03-12 11:06 110a0a3f

View on Github →

chore(Algebra/Group/AddChar): move results (#11312) Currently the definition of additive characters (from an additive to a multiplicative monoid) is hidden away in NumberTheory/LegendreSymbol. These constructions seem to be getting used more widely, e.g. in Yaël's LeanAPAP project; so this PR carves off the parts of NumberTheory/LegendreSymbol/AddCharacter which don't depend on cyclotomic field arithmetic and moves them to Algebra/Group.

Estimated changes

added theorem AddChar.ext
added theorem AddChar.inv_apply
added theorem AddChar.inv_mulShift
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 def AddChar
deleted theorem AddChar.coe_to_fun_apply
deleted theorem AddChar.ext
deleted theorem AddChar.inv_apply
deleted theorem AddChar.inv_mulShift
deleted theorem AddChar.map_add_mul
deleted theorem AddChar.map_nsmul_pow
deleted theorem AddChar.map_zero_one
deleted theorem AddChar.map_zsmul_zpow
deleted def AddChar.mulShift
deleted theorem AddChar.mulShift_apply
deleted theorem AddChar.mulShift_mul
deleted theorem AddChar.mulShift_spec'
deleted theorem AddChar.mulShift_zero
deleted theorem AddChar.mul_apply
deleted theorem AddChar.one_apply
deleted theorem AddChar.pow_mulShift
deleted def AddChar.toMonoidHom
deleted def AddChar