[Merged by Bors] - feat: The descending factorial in ZMod

[mo271]

---

[mo271]

I think this proof would be much nicer using

cast_self_sub {n p : ℕ} (h : n ≤ p) : ((p - n) : ℕ) = - (n : ZMod p)

but I don't know where to put such a lemma best. See [question on zulip].(https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/cast.20from.20.60.E2.84.95.60.20to.20.60ZMod.20p.60.20after.20adding.20or.20subtracting.20p)

[alexjbest]

We already have wilsons theorem somewhere right? Can this be used to simplify the proof there. Or move one version of that theorem to this file if indeed a new file is warranted. Or at least provide a link to wilson in the module doc if nothing else

[mo271]

We already have wilsons theorem somewhere right? Can this be used to simplify the proof there. Or move one version of that theorem to this file if indeed a new file is warranted. Or at least provide a link to wilson in the module doc if nothing else

I think, although a similar statement it has not too much to do with Wilson. When setting n := p - 1, the left hand side is indeed equal to what we see in Wilson, namley (p - 1)! : ZMod p, but the right hand side then simplifies to the same thing and not to -1.
Added a link to Wilson in any case.

[YaelDillies]

Thanks!

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

[github-actions]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

[jcommelin]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style
• Check all files imported