Commit 2023-12-27 20:59 82c60323

View on Github →

feat: Better lemmas for transferring finite sums along equivalences (#9237) Lemmas around this were a mess, throth in terms of names, statement and location. This PR standardises everything to be in Algebra.BigOperators.Basic and changes the lemmas to take in InjOn and SurjOn assumptions where possible (and where impossible make sure the hypotheses are taken in the correct order) and moves the equality of functions hypothesis last. Also add a few lemmas that help fix downstream uses by golfing. From LeanAPAP and LeanCamCombi

Estimated changes

added theorem Equiv.prod_comp
modified theorem Finset.prod_attach
modified theorem Finset.prod_bij'
modified theorem Finset.prod_bij
added theorem Finset.prod_bijective
modified theorem Finset.prod_coe_sort
added theorem Finset.prod_diag
added theorem Finset.prod_equiv
added theorem Finset.prod_fiberwise'
added theorem Finset.prod_fiberwise
modified theorem Finset.prod_ite_one
added theorem Finset.prod_nbij'
added theorem Finset.prod_nbij
modified theorem Fintype.prod_bijective
modified theorem Fintype.prod_equiv
added theorem Fintype.prod_fiberwise
deleted theorem Equiv.prod_comp'
deleted theorem Equiv.prod_comp
deleted theorem Finset.prod_fiberwise
deleted theorem Fintype.prod_fiberwise
deleted theorem Equiv.Perm.signBijAux_inj