Commit 2024-03-15 11:56 b90c18e5

View on Github →

feat: add lemma CanonicallyOrderedCommMonoid.single_le_prod (#11383)

Estimated changes

Modified Mathlib/Algebra/BigOperators/Order.lean

added theorem CanonicallyOrderedCommMonoid.single_le_prod