Theorem Nat.cast_descFactorial_two

Modification history

2023-03-11 15:48
Mathlib/Data/Nat/Factorial/Cast.lean
feat: port Data.Nat.Factorial.Cast (#2801)
Added Nat.cast_descFactorial_twoView on Github →