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 #

@[simp]

nat.double_factorial n is the double factorial of n.

Equations
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)