Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-16 07:24 c75c096a

View on Github →

chore(*): reduce imports (#1033)

chore(*): reduce imports
restoring import in later file
fix import

Estimated changes

Modified src/data/holor.lean

Modified src/order/filter/basic.lean

modified theorem filter.hyperfilter_le_cofinite

modified theorem filter.is_ultrafilter_hyperfilter

modified theorem filter.tendsto_at_top_at_bot

Modified src/order/filter/filter_product.lean

Modified src/order/filter/partial.lean

Modified src/topology/algebra/monoid.lean