Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-31 20:06 acbe099c

View on Github →

feat(*): bump to lean 3.48.0 (#16292) fin n is a structure now.

Estimated changes

Modified archive/imo/imo1987_q1.lean

Modified leanpkg.toml

Modified src/algebra/big_operators/fin.lean

Modified src/algebra/char_zero/quotient.lean

Modified src/algebraic_topology/simplex_category.lean

Modified src/algebraic_topology/split_simplicial_object.lean

Modified src/algebraic_topology/topological_simplex.lean

Modified src/analysis/complex/upper_half_plane/basic.lean

Modified src/analysis/convex/stone_separation.lean

Modified src/combinatorics/composition.lean

Modified src/combinatorics/simple_graph/coloring.lean

Modified src/computability/primrec.lean

Modified src/data/buffer/basic.lean

Modified src/data/countable/defs.lean

Modified src/data/fin/basic.lean

modified def fin.coe_embedding

added theorem fin.coe_eq_coe

modified theorem fin.coe_injective

added def fin.coe_order_embedding

added def fin.equiv_subtype

added theorem fin.equiv_subtype_symm_trans_val_embedding

modified theorem fin.ext_iff

added theorem fin.is_le'

modified theorem fin.is_lt

added theorem fin.max_coe

added theorem fin.min_coe

added theorem fin.mk_eq_mk

deleted theorem fin.mk_eq_subtype_mk

added theorem fin.mk_le_mk

added theorem fin.mk_lt_mk

added def fin.order_iso_subtype

added theorem fin.val_injective

Modified src/data/fin/interval.lean

modified theorem fin.Icc_eq_finset_subtype

modified theorem fin.Ici_eq_finset_subtype

modified theorem fin.Ico_eq_finset_subtype

modified theorem fin.Iic_eq_finset_subtype

modified theorem fin.Iio_eq_finset_subtype

modified theorem fin.Ioc_eq_finset_subtype

modified theorem fin.Ioi_eq_finset_subtype

modified theorem fin.Ioo_eq_finset_subtype

modified theorem fin.map_subtype_embedding_Icc

modified theorem fin.map_subtype_embedding_Ici

modified theorem fin.map_subtype_embedding_Ico

modified theorem fin.map_subtype_embedding_Iic

modified theorem fin.map_subtype_embedding_Iio

modified theorem fin.map_subtype_embedding_Ioc

modified theorem fin.map_subtype_embedding_Ioi

modified theorem fin.map_subtype_embedding_Ioo

Modified src/data/fin/tuple/basic.lean

Modified src/data/finset/basic.lean

added theorem finset.fin_map

added theorem finset.fin_mono

added theorem finset.mem_fin

Modified src/data/finset/sort.lean

Modified src/data/fintype/card.lean

added theorem equiv.prod_comp'

Modified src/data/list/range.lean

Modified src/field_theory/finite/polynomial.lean

Modified src/group_theory/order_of_element.lean

Modified src/linear_algebra/matrix/block.lean

Modified src/linear_algebra/matrix/transvection.lean

Modified src/logic/encodable/basic.lean

Modified src/logic/equiv/fin.lean

Modified src/number_theory/class_number/admissible_abs.lean

Modified src/number_theory/class_number/finite.lean

Modified src/ring_theory/polynomial/basic.lean

Modified src/ring_theory/witt_vector/truncated.lean

Modified src/testing/slim_check/sampleable.lean

Modified src/topology/metric_space/gromov_hausdorff.lean