Theorem IsUnit.natCast_factorial_of_algebra

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_algebraView on Github →