Def Nat.doubleFactorial

Modification history

2023-05-19 16:40

Mathlib/Data/Nat/Factorial/DoubleFactorial.lean

feat: port Data.Nat.Factorial.DoubleFactorial (#4117)

Added Nat.doubleFactorial View on Github →