Theorem Nat.factorial_eq_mul_doubleFactorial

Modification history

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