Commit 2024-01-01 12:02 0d6117a4

View on Github →

feat: Cauchy-Schwarz in semirings (#9371) This is a version of the Cauchy-Schwarz inequality that works in semirings. From LeanAPAP and PFR

Estimated changes

Modified Mathlib/Algebra/BigOperators/Order.lean

added theorem Finset.sum_mul_sq_le_sq_mul_sq

modified theorem Fintype.prod_eq_one_iff_of_le_one

modified theorem Fintype.prod_eq_one_iff_of_one_le