Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-01-05 03:32
0f181024
View on Github →
chore: bump toolchain to v4.16.0-rc1, and merge bump/v4.16.0 (
#20464
)
Estimated changes
Modified
Archive/Imo/Imo2024Q5.lean
Modified
Mathlib.lean
Modified
Mathlib/Algebra/BigOperators/Fin.lean
Modified
Mathlib/Algebra/BigOperators/Group/List.lean
deleted
theorem
Nat.sum_eq_listSum
Modified
Mathlib/Algebra/MvPolynomial/SchwartzZippel.lean
Modified
Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
Modified
Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean
Modified
Mathlib/Analysis/Convex/Continuous.lean
Modified
Mathlib/CategoryTheory/Galois/Decomposition.lean
Modified
Mathlib/Computability/TMToPartrec.lean
Modified
Mathlib/Computability/TuringMachine.lean
Modified
Mathlib/Data/Fin/Basic.lean
modified
theorem
Fin.cast_eq_cast
modified
theorem
Fin.cast_eq_self
modified
theorem
Fin.cast_le_cast
modified
theorem
Fin.cast_lt_cast
modified
theorem
Fin.cast_zero
modified
theorem
Fin.leftInverse_cast
modified
theorem
Fin.rightInverse_cast
Modified
Mathlib/Data/Fin/Tuple/Basic.lean
modified
theorem
Fin.repeat_one
Modified
Mathlib/Data/Fin/Tuple/Take.lean
Modified
Mathlib/Data/Int/Bitwise.lean
Modified
Mathlib/Data/Int/Lemmas.lean
Modified
Mathlib/Data/List/Basic.lean
deleted
theorem
List.getElem_cons
modified
theorem
List.getLast_concat'
deleted
theorem
List.replicate_succ'
Modified
Mathlib/Data/List/Chain.lean
Modified
Mathlib/Data/List/Lemmas.lean
added
theorem
List.Nat.sum_eq_listSum
deleted
theorem
List.countP_flatMap
deleted
theorem
List.count_flatMap
deleted
theorem
List.length_flatMap
Modified
Mathlib/Data/List/Lex.lean
deleted
theorem
List.Lex.not_nil_right
deleted
inductive
List.Lex
modified
theorem
List.lt_iff_lex_lt
deleted
theorem
List.nil_le
deleted
theorem
List.nil_lt_cons
Modified
Mathlib/Data/List/MinMax.lean
Modified
Mathlib/Data/List/Permutation.lean
Modified
Mathlib/Data/Nat/Bitwise.lean
Modified
Mathlib/Data/Nat/Defs.lean
Modified
Mathlib/Data/Num/Basic.lean
Modified
Mathlib/Data/QPF/Multivariate/Constructions/Fix.lean
Modified
Mathlib/Data/String/Basic.lean
Modified
Mathlib/Data/Vector/Basic.lean
Modified
Mathlib/Deprecated/LazyList.lean
Modified
Mathlib/FieldTheory/Finite/GaloisField.lean
Modified
Mathlib/Lean/Expr/Basic.lean
Modified
Mathlib/Lean/Meta/RefinedDiscrTree/Encode.lean
Modified
Mathlib/LinearAlgebra/Dual.lean
Modified
Mathlib/LinearAlgebra/LinearIndependent.lean
Modified
Mathlib/LinearAlgebra/Matrix/SemiringInverse.lean
Modified
Mathlib/Logic/Basic.lean
modified
theorem
imp_forall_iff_forall
Modified
Mathlib/MeasureTheory/Integral/FundThmCalculus.lean
Modified
Mathlib/MeasureTheory/Integral/Marginal.lean
Modified
Mathlib/ModelTheory/Semantics.lean
Modified
Mathlib/NumberTheory/Bernoulli.lean
Modified
Mathlib/NumberTheory/Modular.lean
Modified
Mathlib/Order/Fin/Basic.lean
modified
theorem
Fin.cast_strictMono
Modified
Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean
Modified
Mathlib/RingTheory/Kaehler/JacobiZariski.lean
Modified
Mathlib/RingTheory/Polynomial/Chebyshev.lean
Modified
Mathlib/SetTheory/Ordinal/Notation.lean
modified
def
ONote.ofNat
modified
theorem
ONote.ofNat_one
modified
theorem
ONote.repr_ofNat
modified
theorem
ONote.repr_one
added
theorem
ONote.repr_zero
Modified
Mathlib/Tactic.lean
Modified
Mathlib/Tactic/CC/Addition.lean
Modified
Mathlib/Tactic/CC/Datatypes.lean
Modified
Mathlib/Tactic/CC/MkProof.lean
Modified
Mathlib/Tactic/Common.lean
Deleted
Mathlib/Tactic/DeriveToExpr.lean
deleted
def
Mathlib.Deriving.ToExpr.fixIndType
deleted
def
Mathlib.Deriving.ToExpr.mkAppNTerm
deleted
def
Mathlib.Deriving.ToExpr.mkAuxFunction
deleted
def
Mathlib.Deriving.ToExpr.mkInstanceCmds
deleted
def
Mathlib.Deriving.ToExpr.mkLocalInstanceLetDecls
deleted
def
Mathlib.Deriving.ToExpr.mkMutualBlock
deleted
def
Mathlib.Deriving.ToExpr.mkToExprBody
deleted
def
Mathlib.Deriving.ToExpr.mkToExprHeader
deleted
def
Mathlib.Deriving.ToExpr.mkToExprInstanceCmds
deleted
def
Mathlib.Deriving.ToExpr.mkToExprInstanceHandler
deleted
def
Mathlib.Deriving.ToExpr.mkToLevelBinders
deleted
def
Mathlib.Deriving.ToExpr.mkToTypeExpr
Modified
Mathlib/Tactic/ITauto.lean
Modified
Mathlib/Tactic/Linarith/Frontend.lean
Modified
Mathlib/Tactic/Linter/FlexibleLinter.lean
Modified
Mathlib/Tactic/Linter/HaveLetLinter.lean
Modified
Mathlib/Tactic/SuccessIfFailWithMsg.lean
Modified
Mathlib/Tactic/ToExpr.lean
Modified
Mathlib/Tactic/ToLevel.lean
deleted
def
Lean.ToLevel.imax
deleted
def
Lean.ToLevel.max
Modified
Mathlib/Topology/Category/Profinite/Nobeling.lean
Modified
MathlibTest/DeriveToExpr.lean
Modified
MathlibTest/HashCommandLinter.lean
Modified
MathlibTest/HaveLetLinter.lean
Modified
MathlibTest/TransImports.lean
Modified
MathlibTest/toAdditive.lean
Modified
lake-manifest.json
Modified
lakefile.lean
Modified
lean-toolchain
Modified
scripts/noshake.json