[Merged by Bors] - feat(ZMod): Simple lemmas

[YaelDillies]

From LeanAPAP

---

[github-actions]

PR summary 8ad733242f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ intCast_cast_add
+ intCast_cast_mul
+ intCast_cast_neg
+ intCast_cast_sub
+ inv_one
+ lift_injective
+ mul_val_inv
+ nsmul_zmod_val_inv_nsmul
+ pow_pow_zmod_val_inv
+ pow_zmod_val_inv_pow
+ val_inv_mul
+ val_one''
+ zmod_val_inv_nsmul_nsmul

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>

[Ruben-VandeVelde]

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

[riccardobrasca]

Is this done?

[YaelDillies]

No, sadly to_additive chokes on Inv (ZMod n). cc @fpvandoorn

[riccardobrasca]

OK, maybe add a (very) short explanation that this is the problem (of course if you want to add and issue and link it here even better...).

[riccardobrasca]

Thanks 🎉

If CI passes, please remove the label awaiting-CI and merge this yourself, by adding a comment bors r+.

bors d+

[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:

• Build
• Lint style