Theorem Nat.doubleFactorial_two_mul

Modification history

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