Commit 2025-04-06 04:34 0e1917eb

View on Github →

chore: move batteries and plausible back to main (#23689) These were accidentally left pointing at nightly-testing after the last release.

Estimated changes

Modified Mathlib/Algebra/Order/Floor/Ring.lean

Modified Mathlib/CategoryTheory/Localization/Construction.lean

added theorem CategoryTheory.Localization.Construction.whiskerLeft_natTransExtension

Modified Mathlib/Computability/Encoding.lean

Modified Mathlib/Computability/Partrec.lean

Modified Mathlib/Control/Combinators.lean

Modified Mathlib/Data/Nat/Find.lean

Modified Mathlib/Data/Seq/Parallel.lean

deleted def Computation.parallel.aux1

deleted def Computation.parallel.aux2

Modified Mathlib/MeasureTheory/Function/LpSpace/Basic.lean

Modified Mathlib/MeasureTheory/Function/LpSpace/Indicator.lean

Modified Mathlib/MeasureTheory/Function/SimpleFunc.lean

Modified Mathlib/MeasureTheory/Measure/Content.lean

Modified Mathlib/MeasureTheory/Measure/Hausdorff.lean

Modified Mathlib/MeasureTheory/Measure/Typeclasses/Finite.lean

Modified Mathlib/MeasureTheory/VectorMeasure/Basic.lean

Modified Mathlib/ModelTheory/Bundled.lean

Modified Mathlib/ModelTheory/ElementaryMaps.lean

Modified Mathlib/ModelTheory/ElementarySubstructures.lean

Modified Mathlib/ModelTheory/LanguageMap.lean

Modified Mathlib/ModelTheory/Quotients.lean

Modified Mathlib/ModelTheory/Substructures.lean

Modified Mathlib/ModelTheory/Syntax.lean

Modified Mathlib/ModelTheory/Types.lean

Modified Mathlib/Probability/Process/Filtration.lean

Modified Mathlib/RingTheory/MvPowerSeries/Substitution.lean

Modified lake-manifest.json

Modified lakefile.lean

Modified scripts/nolints.json