Commit 2024-08-04 14:32 1f03949a

View on Github →

feat: Real.exists_natCast_add_one_le_pow_of_one_le (#15074) Necessary for arguments in approaching a power from above

Estimated changes

Modified Mathlib/Data/Nat/Cast/Order/Ring.lean

added theorem Nat.mul_le_pow

added theorem Nat.two_mul_sq_add_one_le_two_pow_two_mul

Modified Mathlib/Data/Real/Archimedean.lean

added theorem Real.exists_natCast_add_one_lt_pow_of_one_lt

Modified Mathlib/Data/Real/Basic.lean

added theorem Real.mul_add_one_le_add_one_pow