Commit 2023-05-18 18:06 362fc59a

View on Github →

feat: port NumberTheory.LegendreSymbol.MulCharacter (#2994) Zulip thread

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/MvPolynomial/Supported.lean

Created Mathlib/NumberTheory/LegendreSymbol/MulCharacter.lean

added theorem MulChar.IsNontrivial.comp

added theorem MulChar.IsNontrivial.sum_eq_zero

added def MulChar.IsNontrivial

added theorem MulChar.IsQuadratic.comp

added theorem MulChar.IsQuadratic.eq_of_eq_coe

added theorem MulChar.IsQuadratic.inv

added theorem MulChar.IsQuadratic.pow_char

added theorem MulChar.IsQuadratic.pow_even

added theorem MulChar.IsQuadratic.pow_odd

added theorem MulChar.IsQuadratic.sq_eq_one

added def MulChar.IsQuadratic

added theorem MulChar.coeToFun_mul

added theorem MulChar.coe_coe

added theorem MulChar.coe_equivToUnitHom

added theorem MulChar.coe_mk

added theorem MulChar.coe_toUnitHom

added theorem MulChar.equiv_unit_hom_symm_coe

added theorem MulChar.ext'

added theorem MulChar.ext

added theorem MulChar.ext_iff

added theorem MulChar.inv_apply'

added theorem MulChar.inv_apply

added theorem MulChar.inv_apply_eq_inv'

added theorem MulChar.inv_apply_eq_inv

added theorem MulChar.inv_mul

added theorem MulChar.isNontrivial_iff

added theorem MulChar.map_nonunit

added theorem MulChar.map_ringChar

added def MulChar.mul

added theorem MulChar.mul_apply

added theorem MulChar.ofUnitHom_coe

added theorem MulChar.ofUnitHom_eq

added theorem MulChar.one_apply_coe

added theorem MulChar.pow_apply'

added theorem MulChar.pow_apply_coe

added def MulChar.ringHomComp

added theorem MulChar.sum_one_eq_card_units

added theorem MulChar.toFun_eq_coe

added def MulChar.toUnitHom

added theorem MulChar.toUnitHom_eq

added structure MulChar