Theorem one_add_mul_le_pow'
Modification history
2021-11-04 07:56
src/algebra/group_power/lemmas.lean
feat(algebra/group_power/order): Sign of an odd/even power without linearity (#10122) …
Modified one_add_mul_le_pow'View on Github →2021-04-28 19:37
src/algebra/group_power/lemmas.lean
chore(*): use `sq` as convention for "squared" (#7368) …
Modified one_add_mul_le_pow'View on Github →2021-01-22 12:52
src/algebra/group_power/lemmas.lean
chore(algebra/group_power): generalize `semiring` version of Bernoulli's inequality (#5831) …
Modified one_add_mul_le_pow'View on Github →