Commit 2022-05-21 03:17 d787d499
View on Github →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
andexists_eq_right_right'
; - add two
simps
attributes.