Commit 2024-06-05 17:08 57599374

View on Github →

feat: add API for multiplicative characters (#13392) This adds some API lemmas for multiplicative characters. We also remove a couple of porting notes (the previous proof lines work again).

Estimated changes

Modified Mathlib/Algebra/Group/Hom/Instances.lean

added theorem MonoidHom.pow_apply

Modified Mathlib/NumberTheory/LegendreSymbol/MulCharacter.lean

added theorem MulChar.equivToUnitHom_mul_apply

modified theorem MulChar.inv_apply'

modified theorem MulChar.inv_apply

modified theorem MulChar.inv_apply_eq_inv'

modified theorem MulChar.map_ringChar

added def MulChar.mulEquivToUnitHom

added theorem MulChar.orderOf_pos

added theorem MulChar.pow_card_eq_one

added theorem MulChar.val_neg_one_eq_one_of_odd_order