Commit 2024-09-03 07:00 70e99da6

View on Github →

feat(AddChar): Additive group structure and double dual embedding (#15441) This PR constructs the additive group structure on AddChar A G (a copy of its multiplicative group structure) and leverages it to define the double dual embedding as a morphism A →+ AddChar (AddChar A M) M. From LeanAPAP

Estimated changes

added theorem AddChar.add_apply
added theorem AddChar.coe_add
added theorem AddChar.coe_nsmul
added theorem AddChar.coe_prod
added theorem AddChar.coe_sum
added theorem AddChar.coe_zero
added theorem AddChar.div_apply'
added theorem AddChar.div_apply
added theorem AddChar.eq_zero_iff
modified theorem AddChar.inv_apply'
modified theorem AddChar.inv_apply
modified theorem AddChar.mul_apply
added theorem AddChar.mul_eq_add
added theorem AddChar.ne_zero_iff
added theorem AddChar.neg_apply'
added theorem AddChar.neg_apply
added theorem AddChar.nsmul_apply
added theorem AddChar.one_eq_zero
modified theorem AddChar.pow_apply
added theorem AddChar.pow_eq_nsmul
added theorem AddChar.prod_apply
added theorem AddChar.prod_eq_sum
added theorem AddChar.sub_apply'
added theorem AddChar.sub_apply
added theorem AddChar.sum_apply
added theorem AddChar.sum_eq_ite
added theorem AddChar.zero_apply