Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2020-04-11 04:27
597704ac
View on Github →
chore(*): switch to lean 3.8.0 (
#2361
) Switch to Lean 3.8.
Estimated changes
Modified
archive/sensitivity.lean
Modified
docs/tutorial/category_theory/intro.lean
Modified
leanpkg.toml
Modified
src/algebra/archimedean.lean
Modified
src/algebra/big_operators.lean
Modified
src/algebra/category/CommRing/colimits.lean
Modified
src/algebra/category/Group/colimits.lean
Modified
src/algebra/category/Module/basic.lean
modified
def
Module.of
Modified
src/algebra/category/Mon/colimits.lean
Modified
src/algebra/char_p.lean
Modified
src/algebra/char_zero.lean
Modified
src/algebra/direct_limit.lean
Modified
src/algebra/euclidean_domain.lean
Modified
src/algebra/field.lean
Modified
src/algebra/group/anti_hom.lean
Modified
src/algebra/group/prod.lean
Modified
src/algebra/group_power.lean
Modified
src/algebra/group_with_zero.lean
Modified
src/algebra/homology/homology.lean
Modified
src/algebra/lie_algebra.lean
Modified
src/algebra/module.lean
modified
theorem
zero_smul
Modified
src/algebra/order_functions.lean
modified
theorem
abs_le_abs
modified
theorem
min_add
modified
theorem
min_sub
Modified
src/algebra/ordered_group.lean
added
theorem
decidable_linear_ordered_add_comm_group.eq_of_abs_sub_nonpos
deleted
theorem
decidable_linear_ordered_comm_group.eq_of_abs_sub_nonpos
modified
theorem
neg_neg_iff_pos
added
def
nonneg_comm_group.to_decidable_linear_ordered_add_comm_group
deleted
def
nonneg_comm_group.to_decidable_linear_ordered_comm_group
Modified
src/algebra/ordered_ring.lean
Modified
src/algebra/pi_instances.lean
Modified
src/algebra/punit_instances.lean
Modified
src/algebra/ring.lean
Modified
src/analysis/calculus/deriv.lean
Modified
src/analysis/calculus/mean_value.lean
Modified
src/analysis/complex/exponential.lean
Modified
src/analysis/normed_space/basic.lean
Modified
src/category/basic.lean
Modified
src/category/equiv_functor.lean
Modified
src/category/monad/writer.lean
Modified
src/category_theory/adjunction/basic.lean
Modified
src/category_theory/adjunction/limits.lean
Modified
src/category_theory/concrete_category/basic.lean
Modified
src/category_theory/concrete_category/unbundled_hom.lean
Modified
src/category_theory/core.lean
Modified
src/category_theory/endomorphism.lean
Modified
src/category_theory/epi_mono.lean
Modified
src/category_theory/equivalence.lean
Modified
src/category_theory/fully_faithful.lean
Modified
src/category_theory/functor.lean
Modified
src/category_theory/functor_category.lean
Modified
src/category_theory/functorial.lean
Modified
src/category_theory/isomorphism.lean
Modified
src/category_theory/limits/cones.lean
Modified
src/category_theory/limits/limits.lean
modified
def
category_theory.limits.colimit.cocone
modified
def
category_theory.limits.limit.cone
Modified
src/category_theory/limits/preserves.lean
Modified
src/category_theory/limits/shapes/equalizers.lean
Modified
src/category_theory/limits/shapes/images.lean
modified
def
category_theory.limits.image.is_image
modified
def
category_theory.limits.image.mono_factorisation
Modified
src/category_theory/limits/shapes/kernels.lean
Modified
src/category_theory/limits/shapes/regular_mono.lean
Modified
src/category_theory/limits/shapes/zero.lean
Modified
src/category_theory/monad/adjunction.lean
Modified
src/category_theory/monad/algebra.lean
Modified
src/category_theory/monad/basic.lean
Modified
src/category_theory/monad/limits.lean
Modified
src/category_theory/monad/types.lean
Modified
src/category_theory/monoidal/category.lean
Modified
src/category_theory/shift.lean
modified
def
category_theory.shift
Modified
src/computability/primrec.lean
Modified
src/computability/turing_machine.lean
Modified
src/data/equiv/denumerable.lean
Modified
src/data/equiv/encodable.lean
Modified
src/data/fin_enum.lean
Modified
src/data/finset.lean
Modified
src/data/finsupp.lean
Modified
src/data/fintype/basic.lean
Modified
src/data/holor.lean
Modified
src/data/list/basic.lean
modified
theorem
list.exists_le_of_sum_le
modified
theorem
list.exists_lt_of_sum_lt
modified
theorem
list.length_pos_of_sum_pos
Modified
src/data/list/defs.lean
Modified
src/data/list/forall2.lean
Modified
src/data/list/min_max.lean
Modified
src/data/list/perm.lean
Modified
src/data/matrix/pequiv.lean
Modified
src/data/mllist.lean
Modified
src/data/monoid_algebra.lean
Modified
src/data/multiset.lean
Modified
src/data/mv_polynomial.lean
Modified
src/data/nat/basic.lean
Modified
src/data/num/lemmas.lean
Modified
src/data/option/defs.lean
Modified
src/data/polynomial.lean
Modified
src/data/prod.lean
modified
theorem
prod.map_fst
added
theorem
prod.map_mk
modified
theorem
prod.map_snd
Modified
src/data/rat/meta_defs.lean
Modified
src/data/rat/order.lean
Modified
src/data/real/basic.lean
Modified
src/data/real/cau_seq.lean
Modified
src/data/real/nnreal.lean
modified
theorem
nnreal.inv_inv
Modified
src/data/seq/wseq.lean
Modified
src/data/set/basic.lean
Modified
src/data/set/function.lean
Modified
src/data/set/intervals/basic.lean
Modified
src/data/set/intervals/unordered_interval.lean
Modified
src/data/sum.lean
Modified
src/data/tree.lean
Modified
src/data/zmod/basic.lean
Modified
src/data/zsqrtd/basic.lean
modified
structure
zsqrtd
Modified
src/deprecated/group.lean
Modified
src/field_theory/perfect_closure.lean
Modified
src/field_theory/subfield.lean
Modified
src/geometry/manifold/manifold.lean
Modified
src/geometry/manifold/mfderiv.lean
Modified
src/group_theory/congruence.lean
Modified
src/group_theory/free_group.lean
Modified
src/group_theory/group_action.lean
modified
theorem
one_smul
Modified
src/group_theory/order_of_element.lean
Modified
src/group_theory/subgroup.lean
Modified
src/group_theory/submonoid.lean
Modified
src/group_theory/sylow.lean
Modified
src/linear_algebra/basis.lean
Modified
src/linear_algebra/dual.lean
Modified
src/linear_algebra/linear_action.lean
Modified
src/logic/relation.lean
Modified
src/measure_theory/borel_space.lean
Modified
src/measure_theory/l1_space.lean
Modified
src/measure_theory/measurable_space.lean
Modified
src/measure_theory/measure_space.lean
Modified
src/measure_theory/simple_func_dense.lean
Modified
src/meta/expr.lean
Modified
src/order/basic.lean
Modified
src/order/bounded_lattice.lean
Modified
src/order/conditionally_complete_lattice.lean
Modified
src/order/filter/basic.lean
Modified
src/order/filter/extr.lean
Modified
src/order/filter/filter_product.lean
modified
theorem
filter.filter_product.abs_def
modified
theorem
filter.filter_product.of_abs
Modified
src/order/lattice.lean
Modified
src/order/lexicographic.lean
Modified
src/order/pilex.lean
Modified
src/ring_theory/adjoin.lean
Modified
src/ring_theory/algebra.lean
Modified
src/ring_theory/free_comm_ring.lean
Modified
src/ring_theory/integral_closure.lean
Modified
src/ring_theory/localization.lean
Modified
src/ring_theory/maps.lean
Modified
src/ring_theory/polynomial.lean
Modified
src/ring_theory/principal_ideal_domain.lean
Modified
src/ring_theory/subring.lean
Modified
src/set_theory/cofinality.lean
Modified
src/set_theory/game.lean
added
def
game.ordered_add_comm_group_game
deleted
def
game.ordered_comm_group_game
Modified
src/set_theory/lists.lean
Modified
src/set_theory/ordinal.lean
Modified
src/set_theory/surreal.lean
Modified
src/tactic/ext.lean
Modified
src/tactic/lift.lean
Modified
src/tactic/norm_num.lean
modified
theorem
norm_num.lt_add_of_pos_helper
Modified
src/tactic/ring_exp.lean
Modified
src/topology/algebra/continuous_functions.lean
Modified
src/topology/algebra/group.lean
Modified
src/topology/algebra/module.lean
Modified
src/topology/algebra/monoid.lean
Modified
src/topology/algebra/open_subgroup.lean
Modified
src/topology/algebra/ordered.lean
modified
theorem
tendsto_abs_at_top_at_top
Modified
src/topology/algebra/uniform_group.lean
Modified
src/topology/bases.lean
Modified
src/topology/instances/ennreal.lean
Modified
src/topology/instances/nnreal.lean
Modified
src/topology/local_extr.lean
Modified
src/topology/metric_space/basic.lean
Modified
src/topology/metric_space/emetric_space.lean
Modified
src/topology/metric_space/hausdorff_distance.lean
Modified
src/topology/metric_space/isometry.lean
Modified
src/topology/order.lean
Modified
src/topology/sheaves/presheaf_of_functions.lean
Modified
src/topology/subset_properties.lean
Modified
test/coinductive.lean
Modified
test/delta_instance.lean
Modified
test/monotonicity/test_cases.lean
Modified
test/tactics.lean
modified
def
dummy
modified
def
right_param
modified
def
wrong_param
Modified
test/traversable.lean
Modified
test/trunc_cases.lean
modified
def
u