Commit 2021-01-22 12:52 faba9cea

View on Github →

chore(algebra/group_power): generalize semiring version of Bernoulli's inequality (#5831) Now one_add_mul_le_pow' assumes 0 ≤ a * a, 0 ≤ (1 + a) * (1 + a), and 0 ≤ 2 + a. Also add a couple of convenience lemmas.

Estimated changes

Modified src/algebra/archimedean.lean

Modified src/algebra/group_power/lemmas.lean

added theorem nat.cast_le_pow_div_sub

added theorem nat.cast_le_pow_sub_div_sub

modified theorem one_add_mul_le_pow'

modified theorem one_add_mul_le_pow

added theorem one_add_mul_sub_le_pow

deleted theorem one_add_sub_mul_le_pow