Commit 2024-07-15 18:29 d6ac8e94

View on Github →

feat(NumberTheory/MulChar): extend API for multiplicative characters (#13939) This adds some more API lemmas for multiplicative characters.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/NumberTheory/MulChar/Basic.lean

added theorem MulChar.ringHomComp_inv

added theorem MulChar.ringHomComp_mul

added theorem MulChar.ringHomComp_one

added theorem MulChar.ringHomComp_pow

Created Mathlib/NumberTheory/MulChar/Lemmas.lean

added theorem MulChar.apply_mem_algebraAdjoin

added theorem MulChar.apply_mem_algebraAdjoin_of_pow_eq_one

added theorem MulChar.apply_mem_rootsOfUnity

added theorem MulChar.apply_mem_rootsOfUnity_of_pow_eq_one

added theorem MulChar.apply_mem_rootsOfUnity_orderOf

added theorem MulChar.eq_iff

added theorem MulChar.exists_apply_eq_pow

added theorem MulChar.exists_mulChar_orderOf

added theorem MulChar.exists_mulChar_orderOf_eq_card_units

added theorem MulChar.ofRootOfUnity_spec

added theorem MulChar.orderOf_dvd_card_sub_one

added def MulChar.starComp

added theorem MulChar.star_apply'

added theorem MulChar.star_apply

added theorem MulChar.star_eq_inv