Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-11-19 23:41 d67e527a

View on Github →

feat(algebra/group_power): prove Bernoulli's inequality for a ≥ -2 (#1709)

  • feat(algebra/group_power): prove Bernoulli's inequality for a ≥ -2
  • Restate inequalities as suggested by @fpvandoorn
  • Fix docs

Estimated changes

added theorem one_add_mul_le_pow'
modified theorem one_add_mul_le_pow
added theorem le_neg_iff_add_nonpos
added theorem neg_le_iff_add_nonneg
added theorem neg_le_self
added theorem self_le_neg