Theorem pow_sum_le_card_mul_sum_pow

Modification history

2024-10-01 14:00
Mathlib/Algebra/Order/Chebyshev.lean
refactor: Generalise special case of Jensen (#11448) …
Added pow_sum_le_card_mul_sum_powView on Github →