Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-01 10:20 49ecc7b0

View on Github →

fix(*): fix things from change tendsto_congr -> tendsto.congr'

Estimated changes

Modified src/analysis/normed_space/deriv.lean

Modified src/analysis/specific_limits.lean

Modified src/data/padics/hensel.lean

Modified src/order/filter/basic.lean

added theorem filter.tendsto.congr'r

deleted theorem filter.tendsto_congr

Modified src/topology/algebra/infinite_sum.lean

Modified src/topology/instances/ennreal.lean