Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-05 13:17 78ffbae0

View on Github →

chore(*): switch to lean 3.6.1 (#2064)

  • chore(*): switch to lean 3.6.0
  • Port src/linear_algebra to Lean 3.6c
  • Port src/ring_theory to Lean 3.6c
  • Port src/algebra and its dependencies to Lean 3.6c
  • Port src/group_theory to Lean 3.6c
  • WIP: Ports part of src/data to Lean 3.6c
  • Port src/data (and dependencies) to Lean 3.6
  • fix set_theory.lists
  • fix ring2
  • fix pell.lean these aren't the cleanest proofs, but pell.lean is kind of a standalone thing.
  • fix dioph.lean
  • Port src/number_theory/sum_four_squares.lean to Lean 3.6c
  • Port src/field_theory to Lean 3.6
  • Port src/computability to Lean 3.6c
  • Port src/measure_theory (and dependencies) to Lean 3.6c
  • fix manifold/real_instances
  • fix analysis/complex/polynomial
  • Fix some compile errors in real_inner_product
  • Upgrade to Lean 3.6.1
  • perf: speed up calls to linarith
  • Reduce instance priorities for potentially noncomputable instances.
  • Remove cyclic instance.
  • Make arguments {implicit} in instances where they can be filled in via unification.
  • Make inner_product_space compile.
  • Style.
  • Port data.nat.modeq
  • Port data.int.parity
  • Port data.int.modeq
  • Port data.real.hyperreal
  • fix(ci): always run git setup step closes #2079 (cherry picked from commit 8a0157dc8dfc946d98eba02417052c3c9556559e)
  • Remove pre-3.6 legacy code.
  • Fix test/monotonicity.lean
  • Fix test/ring_exp.lean
  • Fix test/conv.lean
  • Fix archive/imo1988_q6.lean
  • Fix docs/tutorial/Zmod37.lean
  • Fix archive/sensitivity.lean
  • refactor(algebra/lie_algebra): lie_algebra should not extend lie_ring
  • remove unused argument
  • add doc-string to instance that became a def
  • add docstring
  • Fix linting error ☺
  • Fix data.real.irrational
  • fixing a proof
  • cleaning up proof
  • fix broken proof
  • fix proof
  • fix some more proofs
  • fix
  • fix proofs

Estimated changes

deleted theorem div_div_cancel
deleted theorem div_div_div_cancel_right
modified theorem div_neg
deleted theorem div_right_comm
modified theorem division_ring.inv_eq_iff
modified theorem division_ring.inv_inj
modified theorem field.div_div_cancel
modified theorem field.div_right_comm
modified theorem inv_div
modified theorem inv_div_left
added theorem inv_inv''
deleted theorem inv_inv'
modified theorem inv_involutive'
modified theorem neg_inv
modified theorem is_ring_hom.map_fpow
modified theorem ring_hom.map_fpow
modified theorem neg_sub_neg
modified theorem div_pow
modified theorem division_ring.inv_pow
modified theorem inv_pow'
modified theorem one_div_pow
modified theorem pow_div
modified theorem submodule.coe_sub
modified def vector_space
added theorem pi.sub_apply
added theorem prod.fst_sub
added theorem prod.snd_sub
modified theorem list.mem_enum_from
modified theorem polynomial.degree_map
modified theorem polynomial.map_div
modified theorem polynomial.map_eq_zero
modified theorem polynomial.map_mod
modified theorem polynomial.nat_degree_map
modified theorem rat.cast_div
modified theorem rat.cast_inv
modified theorem rat.cast_mk
modified theorem rat.cast_pow
modified theorem nnreal.inv_inv
deleted theorem set.insert_of_has_insert
modified def perfect_closure.UMP
modified theorem perfect_closure.eq_pth_root
modified theorem dim_of_field
modified def finite_dimensional
modified theorem matrix.rank_diagonal
modified theorem ideal.eq_bot_of_prime
modified theorem ideal.eq_bot_or_top