[Merged by Bors] - feat(Mathlib/Data/Nat/Factorial/NatCast): add IsUnit lemmas#22237
Closed
mariainesdff wants to merge 10 commits intomasterfrom mariainesdff/natCast_factorial
Commits
Commits on Feb 24, 2025
Commits on Mar 5, 2025
- committed
- committed
Commits on Mar 6, 2025
- committed
- committed
- committed
- committed
- committed
