Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-10 00:45 81f97bdf

View on Github →

chore(*): move to lean-3.11.0 (#2632) Related Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/lean.23211.20don't.20unfold.20irred.20defs

Estimated changes

Modified leanpkg.toml

Modified src/algebra/opposites.lean

Modified src/category_theory/limits/shapes/constructions/limits_of_products_and_equalizers.lean

Modified src/category_theory/opposites.lean

Modified src/category_theory/yoneda.lean

Modified src/data/array/lemmas.lean

Modified src/data/complex/basic.lean

Modified src/data/padics/padic_norm.lean

Modified src/data/pfun.lean

Modified src/data/polynomial.lean

modified def polynomial.pow_sub_pow_factor

Modified src/data/real/hyperreal.lean

modified theorem hyperreal.infinitesimal_add

modified theorem hyperreal.infinitesimal_mul

modified theorem hyperreal.infinitesimal_neg

Modified src/geometry/manifold/real_instances.lean

Modified src/measure_theory/bochner_integration.lean

Modified src/set_theory/cofinality.lean

Modified src/topology/metric_space/emetric_space.lean