Theorem IsUnit.natCast_factorial_iff_of_charP

Modification history

2025-03-11 17:25
Mathlib/Data/Nat/Factorial/NatCast.lean
feat(Mathlib/Data/Nat/Factorial/NatCast): add `IsUnit` lemmas (#22237) …
Added IsUnit.natCast_factorial_iff_of_charPView on Github →