Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-02-03 17:43
3685941c
View on Github →
chore: bump toolchain to v4.17.0-rc1 (
#21377
)
Estimated changes
Modified
Mathlib/Algebra/Free.lean
Modified
Mathlib/Algebra/LinearRecurrence.lean
Modified
Mathlib/Algebra/TrivSqZeroExt.lean
Modified
Mathlib/Analysis/Analytic/Composition.lean
Modified
Mathlib/Combinatorics/Enumerative/Composition.lean
Modified
Mathlib/Computability/Primrec.lean
added
theorem
Primrec.list_idxOf
added
theorem
Primrec.list_idxOf₁
deleted
theorem
Primrec.list_indexOf
deleted
theorem
Primrec.list_indexOf₁
Modified
Mathlib/Computability/RegularExpressions.lean
Modified
Mathlib/Data/Fin/Basic.lean
deleted
theorem
Fin.cast_zero
Modified
Mathlib/Data/FinEnum.lean
Modified
Mathlib/Data/Finset/Sort.lean
Modified
Mathlib/Data/List/Basic.lean
added
theorem
List.getElem?_idxOf
deleted
theorem
List.getElem?_indexOf
added
theorem
List.getElem_idxOf
deleted
theorem
List.getElem_indexOf
added
theorem
List.idxOf_append_of_mem
added
theorem
List.idxOf_append_of_not_mem
added
theorem
List.idxOf_cons_eq
added
theorem
List.idxOf_cons_ne
added
theorem
List.idxOf_eq_length_iff
added
theorem
List.idxOf_get
added
theorem
List.idxOf_get?
added
theorem
List.idxOf_inj
added
theorem
List.idxOf_le_length
added
theorem
List.idxOf_lt_length_iff
added
theorem
List.idxOf_of_not_mem
deleted
theorem
List.indexOf_append_of_mem
deleted
theorem
List.indexOf_append_of_not_mem
deleted
theorem
List.indexOf_cons_eq
deleted
theorem
List.indexOf_cons_ne
deleted
theorem
List.indexOf_cons_self
deleted
theorem
List.indexOf_eq_length_iff
deleted
theorem
List.indexOf_get
deleted
theorem
List.indexOf_get?
deleted
theorem
List.indexOf_inj
deleted
theorem
List.indexOf_le_length
deleted
theorem
List.indexOf_lt_length_iff
deleted
theorem
List.indexOf_of_not_mem
Modified
Mathlib/Data/List/Count.lean
Modified
Mathlib/Data/List/Enum.lean
deleted
theorem
List.exists_mem_enum
deleted
theorem
List.exists_mem_enumFrom
added
theorem
List.exists_mem_zipIdx'
added
theorem
List.exists_mem_zipIdx
deleted
theorem
List.forall_mem_enum
deleted
theorem
List.forall_mem_enumFrom
added
theorem
List.forall_mem_zipIdx'
added
theorem
List.forall_mem_zipIdx
deleted
theorem
List.get?_enum
deleted
theorem
List.get?_enumFrom
deleted
theorem
List.get_enum
deleted
theorem
List.get_enumFrom
deleted
theorem
List.mem_enum_iff_get?
deleted
theorem
List.mk_add_mem_enumFrom_iff_get?
deleted
theorem
List.mk_mem_enumFrom_iff_le_and_get?_sub
deleted
theorem
List.mk_mem_enum_iff_get?
Modified
Mathlib/Data/List/FinRange.lean
added
theorem
List.idxOf_finRange
deleted
theorem
List.indexOf_finRange
Modified
Mathlib/Data/List/Forall2.lean
modified
theorem
List.rel_flatMap
Modified
Mathlib/Data/List/Indexes.lean
Modified
Mathlib/Data/List/Intervals.lean
Modified
Mathlib/Data/List/MinMax.lean
Modified
Mathlib/Data/List/Nodup.lean
added
theorem
List.get_idxOf
deleted
theorem
List.get_indexOf
added
theorem
List.idxOf_getElem
deleted
theorem
List.indexOf_getElem
Modified
Mathlib/Data/List/NodupEquivFin.lean
modified
theorem
List.Sorted.coe_getIso_symm_apply
Modified
Mathlib/Data/List/OfFn.lean
added
theorem
List.mem_ofFn'
deleted
theorem
List.mem_ofFn
Modified
Mathlib/Data/List/ProdSigma.lean
Modified
Mathlib/Data/List/Sigma.lean
deleted
theorem
List.nodup_enum_map_fst
added
theorem
List.nodup_zipIdx_map_snd
Modified
Mathlib/Data/List/Sublists.lean
Modified
Mathlib/Data/List/ToFinsupp.lean
added
theorem
List.toFinsupp_eq_sum_mapIdx_single
deleted
theorem
List.toFinsupp_eq_sum_map_enum_single
Modified
Mathlib/Data/Nat/Defs.lean
deleted
theorem
Nat.div_le_div_left
Modified
Mathlib/Data/Nat/Digits.lean
added
theorem
Nat.ofDigits_eq_sum_mapIdx_aux
deleted
theorem
Nat.ofDigits_eq_sum_map_with_index_aux
Modified
Mathlib/Data/Option/Basic.lean
deleted
theorem
Option.map_pmap
deleted
theorem
Option.pmap_eq_map
Modified
Mathlib/Data/Sigma/Basic.lean
Modified
Mathlib/Data/ULift.lean
modified
theorem
PLift.up_inj
modified
theorem
ULift.up_inj
Modified
Mathlib/GroupTheory/Perm/Cycle/Basic.lean
Modified
Mathlib/Lean/Meta/KAbstractPositions.lean
Modified
Mathlib/LinearAlgebra/Multilinear/Basic.lean
Modified
Mathlib/Logic/Equiv/List.lean
Modified
Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
Modified
Mathlib/NumberTheory/Ostrowski.lean
Modified
Mathlib/Order/RelSeries.lean
Modified
Mathlib/Tactic/DeriveTraversable.lean
Modified
Mathlib/Tactic/Linarith/Oracle/FourierMotzkin.lean
Modified
Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm.lean
Modified
Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm/Datatypes.lean
Modified
Mathlib/Tactic/Linarith/Verification.lean
Modified
Mathlib/Tactic/Linter/TextBased.lean
Modified
Mathlib/Tactic/Linter/UnusedTactic.lean
Modified
Mathlib/Tactic/MinImports.lean
Modified
Mathlib/Tactic/MkIffOfInductiveProp.lean
Modified
Mathlib/Tactic/MoveAdd.lean
Modified
Mathlib/Tactic/Widget/StringDiagram.lean
Modified
MathlibTest/fun_prop_dev.lean
Modified
lake-manifest.json
Modified
lean-toolchain
Modified
scripts/noshake.json