Commit 2024-03-17 08:48 2fbad35e

View on Github →

refactor(Algebra/Group/AddChar): reimplement using structures (#11375) Following discussion at #11313 this is an attempt to refactor Algebra/Group/AddChar.lean such that AddChar A M is a structure in its own right rather than a type synonym for Multiplicative A →* M. We also relax typeclass assumptions considerably (only assuming commutativity, etc, where it is really needed) and add some new functionality, e.g. composition with monoid morphisms on either side (MonoidHom.compAddChar and AddChar.compAddMonoidHom).

Estimated changes

Modified Mathlib/Algebra/Group/AddChar.lean

modified def AddChar.IsNontrivial

added theorem AddChar.coe_compAddMonoidHom

added theorem AddChar.coe_mk

deleted theorem AddChar.coe_to_fun_apply

added def AddChar.compAddMonoidHom

modified theorem AddChar.ext

added theorem AddChar.inv_apply'

modified theorem AddChar.inv_apply

modified theorem AddChar.isNontrivial_iff_ne_trivial

modified theorem AddChar.map_add_mul

added theorem AddChar.map_neg_inv

modified theorem AddChar.map_nsmul_pow

modified theorem AddChar.map_zero_one

modified theorem AddChar.map_zsmul_zpow

modified theorem AddChar.mulShift_apply

modified theorem AddChar.mul_apply

modified theorem AddChar.one_apply

added theorem AddChar.pow_apply

added def AddChar.toAddMonoidAddEquiv

added def AddChar.toAddMonoidHom

added def AddChar.toAddMonoidHomEquiv

added theorem AddChar.toAddMonoidHom_apply

modified def AddChar.toMonoidHom

added def AddChar.toMonoidHomEquiv

added def AddChar.toMonoidHomMulEquiv

added theorem AddChar.toMonoidHom_apply

added structure AddChar

deleted def AddChar

added theorem MonoidHom.coe_compAddChar

added def MonoidHom.compAddChar

Modified Mathlib/NumberTheory/LegendreSymbol/AddCharacter.lean