mathlib

69297401 - refactor(algebra/big_operators/finprod) move finiteness assumptions to be final parameters (#7196)

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.