Theorem pow_add_mul_le_add_pow_of_sq_nonneg

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_of_sq_nonnegView on Github →