Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-12-06 17:16 a3a2faa9

View on Github →

feat(algebra/big_operators): add renameing rules under bijection

Estimated changes

Modified algebra/big_operators.lean

added theorem finset.prod_attach

added theorem finset.prod_bij

added theorem finset.prod_bij_ne_one

Modified data/finset.lean

added theorem finset.attach_image_val