Commit 2023-11-08 20:09 b4384456

View on Github →

feat(Algebra/BigOperators): add mul_le_prod/add_le_sum (#8188)

Estimated changes

added theorem Finset.mul_le_prod