Commit 2023-04-11 12:30 fa14d83c

View on Github →

feat: port Algebra.Order.Chebyshev (#3376)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Order/Chebyshev.lean

added theorem Antivary.card_mul_sum_le_sum_mul_sum

added theorem Antivary.card_smul_sum_le_sum_smul_sum

added theorem AntivaryOn.card_mul_sum_le_sum_mul_sum

added theorem AntivaryOn.card_smul_sum_le_sum_smul_sum

added theorem Monovary.sum_mul_sum_le_card_mul_sum

added theorem Monovary.sum_smul_sum_le_card_smul_sum

added theorem MonovaryOn.sum_mul_sum_le_card_mul_sum

added theorem MonovaryOn.sum_smul_sum_le_card_smul_sum

added theorem sq_sum_le_card_mul_sum_sq

added theorem sum_div_card_sq_le_sum_sq_div_card