Commit 2022-05-21 03:17 d787d499

feat(algebra/big_operators): add finset.prod_comm' (#14257)

• add a "dependent" version of finset.prod_comm;
• use it to prove the original lemma;
• slightly generalize exists_eq_right_right and exists_eq_right_right';
• add two simps attributes.