Invertibility of factorials #
This file contains lemmas providing sufficient conditions for the cast of n!
to a (semi)ring A
to be a unit.
theorem
IsUnit.natCast_of_isNilpotent_of_coprime
{A : Type u_1}
[CommRing A]
{n p : ℕ}
(hp : IsNilpotent ↑p)
(h : p.Coprime n)
:
IsUnit ↑n