Commit 2025-11-17 15:40 c316eae7

View on Github →

feat: add a version of Bernoulli's inequality (#31502) Motivated by #31492

Estimated changes

Modified Mathlib/Algebra/Order/Archimedean/Basic.lean

Modified Mathlib/Algebra/Order/Ring/Pow.lean

added theorem Commute.pow_add_mul_le_add_pow

added theorem Commute.pow_add_mul_le_add_pow_of_sq_nonneg

added theorem one_add_le_pow_of_two_add_nonneg

modified theorem one_add_mul_le_pow'

added theorem one_add_mul_le_pow_of_sq_nonneg

added theorem pow_add_mul_le_add_pow

added theorem pow_add_mul_le_add_pow_of_sq_nonneg