Commit 2021-04-22 20:22 69297401

refactor(algebra/big_operators/finprod) move finiteness assumptions to be final parameters (#7196) This PR takes all the finiteness hypotheses in finprod.lean and moves them back to be the last parameters of their lemmas. this only affects a handful of them because the API is small, and nothing else relies on it yet. This change is to allow for easier rewriting in cases where finiteness goals can be easily discharged, such as where a fintype instance is present. I also added t as an explicit parameter in finprod_mem_inter_mul_diff and the primed version, since it may be useful to invoke the lemma in cases where it can't be inferred, such as when rewriting in reverse.