Commit 2025-03-11 17:25 20239f6c

View on Github →

feat(Mathlib/Data/Nat/Factorial/NatCast): add IsUnit lemmas (#22237) Co'authored-by: Eric Wieser eric-wieser

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Nat/Factorial/NatCast.lean

added theorem IsUnit.natCast_factorial_iff_of_charP

added theorem IsUnit.natCast_factorial_of_algebra

added theorem IsUnit.natCast_factorial_of_le

added theorem IsUnit.natCast_factorial_of_lt