mathlib3 documentation

data.nat.factorial.double_factorial

Double factorials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines the double factorial, n‼ := n * (n - 2) * (n - 4) * ....

Main declarations #

nat.double_factorial: The double factorial.

@[simp]

def nat.double_factorial :

nat.double_factorial n is the double factorial of n.

Equations

(k + 2).double_factorial = (k + 2) * k.double_factorial
1.double_factorial = 1
0.double_factorial = 1

theorem nat.double_factorial_add_two (n : ℕ) :

(n + 2).double_factorial = (n + 2) * n.double_factorial

theorem nat.double_factorial_add_one (n : ℕ) :

(n + 1).double_factorial = (n + 1) * (n - 1).double_factorial

theorem nat.factorial_eq_mul_double_factorial (n : ℕ) :

(n + 1).factorial = (n + 1).double_factorial * n.double_factorial

theorem nat.double_factorial_two_mul (n : ℕ) :

(2 * n).double_factorial = 2 ^ n * n.factorial

theorem nat.double_factorial_eq_prod_even (n : ℕ) :

(2 * n).double_factorial = (finset.range n).prod (λ (i : ℕ), 2 * (i + 1))

theorem nat.double_factorial_eq_prod_odd (n : ℕ) :

(2 * n + 1).double_factorial = (finset.range n).prod (λ (i : ℕ), 2 * (i + 1) + 1)