Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes