Theorem IsUnit.natCast_factorial_of_le

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_of_le View on Github →