Commit 2023-10-25 11:20 7c069f7f
View on Github →feat(Algebra/BigOperators/Order): prod_lt_prod (#7844) Add a product variant of mul_lt_mul, following the pattern of Finset.prod_lt_prod'. This fills in a gap between Finset.prod_le_prod, Finset.prod_le_prod' and Finset.prod_lt_prod'.