Commit 2023-12-26 03:42 61efe6de

View on Github →

feat: The double factorial is positive (#9102) and other basic results. Also include a positivity extension to encode that new result. From LeanAPAP

Estimated changes

Modified Mathlib/Data/Nat/Factorial/Basic.lean

added theorem Nat.factorial_two_mul_le

added theorem Nat.two_pow_mul_factorial_le_factorial_two_mul

Modified Mathlib/Data/Nat/Factorial/BigOperators.lean

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

added def Mathlib.Meta.Positivity.evalDoubleFactorial

added theorem Nat.doubleFactorial_le_factorial

added theorem Nat.doubleFactorial_pos