Theorem Nat.two_pow_mul_factorial_le_factorial_two_mul

Modification history

2025-07-15 09:22
Mathlib/Data/Nat/Factorial/Basic.lean
chore: remove whitespace (#26963) …
Modified Nat.two_pow_mul_factorial_le_factorial_two_mulView on Github →
2023-12-26 03:42
Mathlib/Data/Nat/Factorial/Basic.lean
feat: The double factorial is positive (#9102) …
Added Nat.two_pow_mul_factorial_le_factorial_two_mulView on Github →