Theorem Nat.doubleFactorial_eq_prod_odd

Modification history

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