Commit 2023-03-11 15:48 2fb506f6

View on Github →

feat: port Data.Nat.Factorial.Cast (#2801)

Estimated changes

Modified Mathlib.lean

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

added theorem Nat.cast_ascFactorial

added theorem Nat.cast_descFactorial

added theorem Nat.cast_descFactorial_two

added theorem Nat.cast_factorial