Commit 2023-05-19 16:40 8c878fe1

View on Github →

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

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Nat/Factorial/DoubleFactorial.lean

added def Nat.doubleFactorial

added theorem Nat.doubleFactorial_add_one

added theorem Nat.doubleFactorial_add_two

added theorem Nat.doubleFactorial_eq_prod_even

added theorem Nat.doubleFactorial_eq_prod_odd

added theorem Nat.doubleFactorial_two_mul

added theorem Nat.factorial_eq_mul_doubleFactorial