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.