Commit 2024-09-28 19:13 5a5f390c

View on Github →

feat(AddChar): more basic lemmas (#17018) Also unsimp AddChar.div_apply/AddChar.sub_apply because it doesn't do the right thing in my application. From LeanAPAP

Estimated changes

Modified Mathlib/Algebra/Group/AddChar.lean

added theorem AddChar.coe_eq_one

modified theorem AddChar.div_apply

modified theorem AddChar.sub_apply

added theorem AddChar.toAddMonoidHomEquiv_symm_zero

added theorem AddChar.toAddMonoidHomEquiv_zero

added theorem AddChar.toMonoidHomEquiv_add

added theorem AddChar.toMonoidHomEquiv_symm_mul

added theorem AddChar.toMonoidHomEquiv_symm_one

added theorem AddChar.toMonoidHomEquiv_zero

added theorem AddChar.zpow_apply

added theorem AddChar.zsmul_apply