Theorem one_add_mul_le_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 one_add_mul_le_pow_of_sq_nonnegView on Github →