Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-13 06:01 82a53736

View on Github →

feat(*): update to Lean 3.49 (#17470) In https://github.com/leanprover-community/lean/pull/779 we backported the Lean 4 definition of min and max in linear_order.

Estimated changes

Modified counterexamples/zero_divisors_in_add_monoid_algebras.lean

modified theorem zero_divisors_of_periodic

Modified leanpkg.toml

Modified src/algebra/order/floor.lean

Modified src/computability/primrec.lean

modified theorem primrec.nat_max

Modified src/data/list/basic.lean

deleted theorem list.foldl_combinator_K

Modified src/data/list/min_max.lean

Modified src/measure_theory/constructions/borel_space.lean

Modified src/number_theory/lucas_lehmer.lean

Modified src/order/basic.lean

modified theorem max_def'

added theorem max_def_lt

modified theorem min_def'

added theorem min_def_lt

Modified src/order/lattice.lean

Modified src/set_theory/cardinal/divisibility.lean

Modified src/tactic/fin_cases.lean

Modified src/topology/path_connected.lean