Documentation

Mathlib.Data.ZMod.Factorial

Facts about factorials in ZMod #

We collect facts about factorials in context of modular arithmetic.

Main statements #

See also #

For the prime case and involving factorial rather than descFactorial, see Wilson's theorem: