DoubleFactorial

📁 Source: Mathlib/Data/Nat/Factorial/DoubleFactorial.lean

Statistics

Metric	Count
Definitions evalDoubleFactorial, doubleFactorial, «term_‼»	3
Theorems doubleFactorial_add_one, doubleFactorial_add_two, doubleFactorial_eq_prod_even, doubleFactorial_eq_prod_odd, doubleFactorial_le_factorial, doubleFactorial_pos, doubleFactorial_two_mul, factorial_eq_mul_doubleFactorial	8
Total	11

Mathlib.Meta.Positivity

Definitions

Name	Category	Theorems
evalDoubleFactorial 📖	CompOp	—

Nat

Definitions

Name	Category	Theorems
doubleFactorial 📖	CompOp	15 math math: Real.Gamma_nat_add_half, factorial_eq_mul_doubleFactorial, Polynomial.coeff_hermite_explicit, InnerProductSpace.volume_ball_of_dim_odd, Polynomial.coeff_hermite_of_even_add, Real.Gamma_nat_add_one_add_half, doubleFactorial_eq_prod_odd, doubleFactorial_pos, doubleFactorial_add_one, doubleFactorial_add_two, Polynomial.coeff_hermite, doubleFactorial_two_mul, doubleFactorial_le_factorial, doubleFactorial_eq_prod_even, InnerProductSpace.volume_closedBall_of_dim_odd
«term_‼» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
doubleFactorial_add_one 📖	mathematical	—	doubleFactorial	—	—
doubleFactorial_add_two 📖	mathematical	—	doubleFactorial	—	—
doubleFactorial_eq_prod_even 📖	mathematical	—	doubleFactorial Finset.prod instCommMonoid Finset.range	—	Finset.prod_range_succ mul_comm Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.zero_mul
doubleFactorial_eq_prod_odd 📖	mathematical	—	doubleFactorial Finset.prod instCommMonoid Finset.range	—	Finset.prod_range_succ mul_comm Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw
doubleFactorial_le_factorial 📖	mathematical	—	doubleFactorial factorial	—	le_rfl factorial_eq_mul_doubleFactorial doubleFactorial_pos
doubleFactorial_pos 📖	mathematical	—	doubleFactorial	—	zero_lt_one instZeroLEOneClass mul_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono
doubleFactorial_two_mul 📖	mathematical	—	doubleFactorial Monoid.toNatPow instMonoid factorial	—	mul_add Distrib.leftDistribClass mul_one doubleFactorial_add_two factorial.eq_2 pow_succ Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.pow_prod_atom Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add
factorial_eq_mul_doubleFactorial 📖	mathematical	—	factorial doubleFactorial	—	doubleFactorial_add_two factorial.eq_2 mul_comm mul_assoc

---

← Back to Index