Commit 2021-03-27 03:05 5eead090
View on Github →feat(algebra/big_operators/basic): add lemmas for a product with two non one factors (#6826)
Add another version of prod_eq_one and 3 versions of prod_eq_double, a lemma that says a product with only 2 non one factors is equal to the product of the 2 factors.