Mathlib Changelog
v4
Changelog
About
Github
Commit
2026-06-18 23:59
360da6fa
View on Github →
chore: bump toolchain to v4.32.0-rc1 (
#40732
)
Estimated changes
Modified
Counterexamples/DirectSumIsInternal.lean
added
def
Counterexample.withSign.independent
deleted
theorem
Counterexample.withSign.independent
Modified
Mathlib/Algebra/Category/Grp/Basic.lean
Modified
Mathlib/Algebra/Module/Presentation/Basic.lean
Modified
Mathlib/Algebra/Order/AbsoluteValue/Basic.lean
Modified
Mathlib/Algebra/Order/Algebra.lean
Modified
Mathlib/Algebra/Order/BigOperators/Expect.lean
Modified
Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean
Modified
Mathlib/Algebra/Order/Field/Basic.lean
Modified
Mathlib/Algebra/Order/Field/Power.lean
Modified
Mathlib/Algebra/Order/Floor/Extended.lean
Modified
Mathlib/Algebra/Order/Floor/Ring.lean
Modified
Mathlib/Algebra/Order/Interval/Basic.lean
Modified
Mathlib/Algebra/Order/Module/Field.lean
Modified
Mathlib/Analysis/Complex/Exponential.lean
Modified
Mathlib/Analysis/Complex/Order.lean
Modified
Mathlib/Analysis/Complex/Trigonometric.lean
Modified
Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean
Modified
Mathlib/Analysis/Normed/Group/Basic.lean
Modified
Mathlib/Analysis/Real/Sqrt.lean
Modified
Mathlib/Analysis/SpecialFunctions/Bernstein.lean
Modified
Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
Modified
Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
Modified
Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
Modified
Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
Modified
Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean
Modified
Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
Modified
Mathlib/Analysis/SpecialFunctions/Trigonometric/DerivHyp.lean
Modified
Mathlib/CategoryTheory/Bicategory/Basic.lean
Modified
Mathlib/CategoryTheory/Category/Cat.lean
Modified
Mathlib/CategoryTheory/Category/Preorder.lean
Modified
Mathlib/CategoryTheory/Category/Quiv.lean
Modified
Mathlib/CategoryTheory/Category/ReflQuiv.lean
Modified
Mathlib/CategoryTheory/FiberedCategory/BasedCategory.lean
Modified
Mathlib/CategoryTheory/FiberedCategory/HasFibers.lean
Modified
Mathlib/CategoryTheory/Groupoid/Grpd/Basic.lean
Modified
Mathlib/CategoryTheory/Limits/Chosen/End.lean
Modified
Mathlib/CategoryTheory/Limits/Creates.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean
Modified
Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean
Modified
Mathlib/CategoryTheory/MorphismProperty/Local.lean
added
theorem
CategoryTheory.MorphismProperty.of_zeroHypercover_source
added
theorem
CategoryTheory.MorphismProperty.of_zeroHypercover_target
Modified
Mathlib/Combinatorics/Enumerative/DyckWord.lean
Modified
Mathlib/Combinatorics/Hindman.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Triangle/Removal.lean
Modified
Mathlib/Computability/Partrec.lean
Modified
Mathlib/Data/ENNReal/Basic.lean
Modified
Mathlib/Data/ENNReal/Real.lean
Modified
Mathlib/Data/EReal/Basic.lean
Modified
Mathlib/Data/EReal/Inv.lean
Modified
Mathlib/Data/EReal/Operations.lean
Modified
Mathlib/Data/Fin/Tuple/Reflection.lean
Modified
Mathlib/Data/NNReal/Defs.lean
Modified
Mathlib/Data/Nat/Factorial/DoubleFactorial.lean
Modified
Mathlib/Data/Nat/Find.lean
Modified
Mathlib/Data/Nat/Sqrt.lean
deleted
theorem
Nat.lt_succ_sqrt
deleted
theorem
Nat.sqrt.iter_sq_le
deleted
theorem
Nat.sqrt.lt_iter_succ_sq
deleted
theorem
Nat.sqrt_le
modified
theorem
Nat.sqrt_one
modified
theorem
Nat.sqrt_two
modified
theorem
Nat.sqrt_zero
Modified
Mathlib/Data/Nat/Totient.lean
Modified
Mathlib/Data/PFunctor/Univariate/Basic.lean
Modified
Mathlib/Data/Rat/Cast/Order.lean
Modified
Mathlib/FieldTheory/Galois/IsGaloisGroup.lean
Modified
Mathlib/Geometry/Euclidean/Altitude.lean
Modified
Mathlib/Geometry/RingedSpace/Basic.lean
Modified
Mathlib/Init.lean
Modified
Mathlib/Lean/MessageData/ForExprs.lean
Modified
Mathlib/Lean/Meta/RefinedDiscrTree/Encode.lean
Modified
Mathlib/MeasureTheory/Covering/Besicovitch.lean
Modified
Mathlib/MeasureTheory/Integral/Bochner/Basic.lean
Modified
Mathlib/MeasureTheory/Measure/Real.lean
Modified
Mathlib/ModelTheory/Basic.lean
Modified
Mathlib/NumberTheory/ArithmeticFunction/Misc.lean
Modified
Mathlib/NumberTheory/ArithmeticFunction/Zeta.lean
Modified
Mathlib/NumberTheory/Height/Basic.lean
Modified
Mathlib/NumberTheory/Height/NumberField.lean
Modified
Mathlib/NumberTheory/Height/Projectivization.lean
Modified
Mathlib/NumberTheory/LucasLehmer.lean
Modified
Mathlib/NumberTheory/Padics/Hensel.lean
Modified
Mathlib/NumberTheory/SelbergSieve.lean
Modified
Mathlib/SetTheory/Ordinal/Univ.lean
Modified
Mathlib/SetTheory/ZFC/PSet.lean
Modified
Mathlib/Tactic/Algebra/Basic.lean
Modified
Mathlib/Tactic/CrossRefAttribute.lean
Modified
Mathlib/Tactic/DefEqAbuse.lean
Modified
Mathlib/Tactic/DeprecateTo.lean
Modified
Mathlib/Tactic/DeriveEncodable.lean
Modified
Mathlib/Tactic/FieldSimp.lean
Modified
Mathlib/Tactic/FieldSimp/Lemmas.lean
Modified
Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm/Gauss.lean
Modified
Mathlib/Tactic/LinearCombinationPrime.lean
Modified
Mathlib/Tactic/Linter/HaveLetLinter.lean
Modified
Mathlib/Tactic/Linter/Style.lean
Modified
Mathlib/Tactic/Linter/Whitespace.lean
Modified
Mathlib/Tactic/NormNum/Core.lean
Modified
Mathlib/Tactic/NormNum/Irrational.lean
modified
def
Tactic.NormNum.evalIrrationalRpow
Modified
Mathlib/Tactic/Positivity/Basic.lean
modified
def
Mathlib.Meta.Positivity.evalAdd
modified
def
Mathlib.Meta.Positivity.evalIntDiv
Modified
Mathlib/Tactic/Positivity/Core.lean
Modified
Mathlib/Tactic/Positivity/Finset.lean
Modified
Mathlib/Tactic/ReduceModChar.lean
Modified
Mathlib/Tactic/Ring/Basic.lean
Modified
Mathlib/Tactic/Ring/Common.lean
Modified
Mathlib/Tactic/Ring/Compare.lean
Modified
Mathlib/Tactic/Simproc/ExistsAndEq.lean
Modified
Mathlib/Tactic/TacticAnalysis/Declarations.lean
Modified
Mathlib/Tactic/Translate/Core.lean
Modified
Mathlib/Tactic/Translate/Reorder.lean
Modified
Mathlib/Tactic/Variable.lean
Modified
Mathlib/Topology/Algebra/InfiniteSum/Order.lean
Modified
Mathlib/Topology/Category/CompHausLike/Limits.lean
Modified
Mathlib/Topology/ContinuousMap/Algebra.lean
Modified
Mathlib/Topology/MetricSpace/Bounded.lean
Modified
Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
Modified
Mathlib/Util/CountHeartbeats.lean
Modified
Mathlib/Util/GetAllModules.lean
Modified
Mathlib/Util/WhatsNew.lean
Modified
MathlibTest/Attribute/ToAdditive/Basic.lean
Modified
MathlibTest/Attribute/ToDual.lean
Modified
MathlibTest/CategoryTheory/CategoryStar.lean
Modified
MathlibTest/Linter/DocPrime.lean
Modified
MathlibTest/MinImports.lean
Modified
MathlibTest/Simps.lean
Modified
MathlibTest/Subsingleton.lean
Modified
MathlibTest/Tactic/Says/Basic.lean
Modified
MathlibTest/UnusedTactic.lean
Modified
MathlibTest/globalAttributeIn.lean
Modified
MathlibTest/symm.lean
Modified
lake-manifest.json
Modified
lean-toolchain
Modified
scripts/create_deprecated_modules.lean
Modified
scripts/lint-style.lean
Modified
scripts/mk_all.lean