Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-11 17:36 b7107717

View on Github →

chore(*): update to 3.38.0c (#11371)

Estimated changes

Modified archive/100-theorems-list/83_friendship_graphs.lean

Modified leanpkg.toml

Modified src/algebra/monoid_algebra/basic.lean

Modified src/algebra/pointwise.lean

Modified src/analysis/analytic/basic.lean

Modified src/category_theory/limits/shapes/wide_pullbacks.lean

Modified src/combinatorics/hall/finite.lean

Modified src/combinatorics/simple_graph/basic.lean

added theorem simple_graph.mem_neighbor_set'

Modified src/computability/tm_to_partrec.lean

Modified src/computability/turing_machine.lean

Modified src/data/dfinsupp/basic.lean

Modified src/data/equiv/basic.lean

Modified src/data/equiv/set.lean

Modified src/data/finset/basic.lean

modified theorem finset.piecewise_coe

Modified src/data/finset/fold.lean

Modified src/data/finsupp/multiset.lean

Modified src/data/fintype/basic.lean

added theorem fintype.card_congr'

added theorem set.to_finset_congr

Modified src/data/fintype/fin.lean

Modified src/data/list/basic.lean

added theorem list.filter_congr'

deleted theorem list.filter_congr

added theorem list.map_id''

Modified src/data/list/count.lean

Modified src/data/list/intervals.lean

Modified src/data/list/lattice.lean

Modified src/data/list/nodup.lean

Modified src/data/list/perm.lean

Modified src/data/list/permutation.lean

Modified src/data/matrix/block.lean

Modified src/data/multiset/basic.lean

added theorem multiset.map_comp_cons

modified theorem multiset.map_congr

Modified src/data/multiset/nodup.lean

Modified src/data/multiset/pi.lean

added theorem multiset.pi.cons_ext

Modified src/data/multiset/powerset.lean

Modified src/data/mv_polynomial/basic.lean

Modified src/data/mv_polynomial/rename.lean

Modified src/data/nat/count.lean

Modified src/data/nat/enat.lean

Modified src/data/option/basic.lean

modified theorem option.guard_eq_some'

Modified src/data/pequiv.lean

Modified src/data/pi.lean

Modified src/data/polynomial/basic.lean

Modified src/data/polynomial/derivative.lean

Modified src/data/semiquot.lean

Modified src/data/set/finite.lean

Modified src/data/sym/basic.lean

Modified src/data/vector/basic.lean

Modified src/geometry/manifold/instances/real.lean

Modified src/group_theory/commuting_probability.lean

Modified src/group_theory/sylow.lean

Modified src/linear_algebra/affine_space/basis.lean

Modified src/linear_algebra/affine_space/combination.lean

Modified src/logic/function/basic.lean

Modified src/measure_theory/covering/besicovitch.lean

Modified src/measure_theory/integral/lebesgue.lean

Modified src/measure_theory/measure/hausdorff.lean

Modified src/measure_theory/measure/measure_space.lean

Modified src/measure_theory/measure/outer_measure.lean

Modified src/measure_theory/probability_mass_function/constructions.lean

Modified src/order/filter/lift.lean

Modified src/ring_theory/polynomial/symmetric.lean

Modified src/ring_theory/polynomial_algebra.lean

Modified src/ring_theory/power_series/basic.lean

Modified src/ring_theory/unique_factorization_domain.lean

Modified src/set_theory/ordinal_arithmetic.lean

Modified src/tactic/cache.lean

Modified src/tactic/split_ifs.lean

Modified src/topology/algebra/uniform_field.lean

Modified src/topology/bases.lean

Modified src/topology/homotopy/fundamental_groupoid.lean

Modified src/topology/metric_space/basic.lean

Modified src/topology/path_connected.lean