Theorem one_add_mul_le_pow'

Modification history

2026-05-17 20:27
Mathlib/Algebra/Order/Ring/Pow.lean
chore: remove declarations deprecated between 2021-05-15 and 2025-11-15 (#39405) …
Deleted one_add_mul_le_pow'View on Github →
2025-11-17 15:40
Mathlib/Algebra/Order/Ring/Pow.lean
feat: add a version of Bernoulli's inequality (#31502) …
Modified one_add_mul_le_pow'View on Github →
2024-01-09 08:14
Mathlib/Algebra/GroupPower/Lemmas.lean
chore: Move Bernoulli's inequality (#9456) …
Modified one_add_mul_le_pow'View on Github →
2022-12-19 11:23
Mathlib/Algebra/GroupPower/Lemmas.lean
feat port Algebra.GroupPower.Lemmas (#1055) …
Added one_add_mul_le_pow'View on Github →