Theorem Nat.doubleFactorial_add_one

Modification history

2023-05-19 16:40
Mathlib/Data/Nat/Factorial/DoubleFactorial.lean
feat: port Data.Nat.Factorial.DoubleFactorial (#4117)
Added Nat.doubleFactorial_add_oneView on Github →