Theorem Commute.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 Commute.pow_add_mul_le_add_powView on Github →