Commit 2026-09-07 07:56 dbe98010

feat(Algebra/Order/BigOperators/Group/Finset): generalise exists_one_lt_of_prod_one_of_exists_ne_one (#43500) and add its dual. I couldn't get to_dual to generate the dual, I presume because the rest of this file hasn't been to_dual'd yet. It's probably easier to do that in its own PR. The generalisation here is that it uses weaker typeclass assumptions now - MulLeftMono rather than IsOrderedCancelMonoid, ie it no longer requires cancellativity.