Theorem pow_add_mul_le_add_pow

Modification history

2025-11-17 15:40

Mathlib/Algebra/Order/Ring/Pow.lean

feat: add a version of Bernoulli's inequality (#31502) …

Added pow_add_mul_le_add_pow View on Github →