Commit 2021-02-05 08:47 53914334
View on Github →feat(algebra/group_power/basic): pow_add_pow_le
(#6037)
For natural n ≠ 0
and nonnegative x, y
in an ordered_semiring
, x ^ n + y ^ n ≤ (x + y) ^ n
.
feat(algebra/group_power/basic): pow_add_pow_le
(#6037)
For natural n ≠ 0
and nonnegative x, y
in an ordered_semiring
, x ^ n + y ^ n ≤ (x + y) ^ n
.