Theorem Finset.single_le_prod_of_canonicallyOrdered

Modification history

2025-09-07 05:34
Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
chore: remove `CanonicallyOrderedAddCommMonoid` (#29377) …
Added Finset.single_le_prod_of_canonicallyOrderedView on Github →