Commit 2024-05-07 12:53 77f39e12

View on Github →

feat: FloorRing.exists_prime_mul_pow_div_factorial_lt_one (#12191) A few technical lemmas in support of Lindemann-Weierstrass.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Order/Floor/Prime.lean

added theorem FloorRing.exists_prime_mul_pow_div_factorial_lt_one

added theorem FloorRing.exists_prime_mul_pow_lt_factorial

Modified Mathlib/Data/Nat/Prime.lean

added theorem Nat.exists_mul_pow_lt_factorial

added theorem Nat.exists_pow_lt_factorial

added theorem Nat.exists_prime_mul_pow_lt_factorial