mathlib

5eead090 - feat(algebra/big_operators/basic): add lemmas for a product with two non one factors (#6826)

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. Co-authored-by: paulvanwamelen <30371019+paulvanwamelen@users.noreply.github.com>