Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-12-13 12:21 421c332e

View on Github →

fix(algebra/big_operators): congruence rules need to provide equations for all rewritable positions

Estimated changes

Modified algebra/big_operators.lean

modified theorem finset.prod_congr

Modified algebra/linear_algebra/basic.lean

Modified analysis/topology/infinite_sum.lean

Modified data/finsupp.lean