[Merged by Bors] - feat: ZMod-module lemmas

[YaelDillies]

From PFR

---

I am not a huge fan of the names I came up with, so I would gladly take suggestions.

[github-actions]

PR summary 5016bbbb2b

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ ZModModule.add_add_add_cancel
+ ZModModule.add_self
+ ZModModule.char_ne_one
+ ZModModule.char_nsmul_eq_zero
+ ZModModule.neg_eq_self
+ ZModModule.periodicPts_add_left
+ ZModModule.sub_eq_add
+ ZModModule.two_le_char

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[mathlib-bors]

✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[YaelDillies]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Lint style
• Build