Commit 2025-12-02 11:41 1199f1de

View on Github →

chore: tidy various files (#32332)

Estimated changes

Modified Counterexamples/PeanoCurve.lean

Modified Mathlib/Analysis/Calculus/Deriv/Basic.lean

Modified Mathlib/Analysis/Calculus/Deriv/Comp.lean

Modified Mathlib/Analysis/Calculus/Deriv/Mul.lean

Modified Mathlib/Analysis/Calculus/Deriv/Polynomial.lean

Modified Mathlib/Analysis/Calculus/Deriv/Slope.lean

Modified Mathlib/Analysis/Calculus/Deriv/ZPow.lean

Modified Mathlib/Analysis/Complex/ValueDistribution/CountingFunction.lean

Modified Mathlib/Analysis/Distribution/FourierSchwartz.lean

Modified Mathlib/Analysis/Distribution/TemperateGrowth.lean

Modified Mathlib/Analysis/Real/OfDigits.lean

Modified Mathlib/CategoryTheory/Limits/VanKampen.lean

Modified Mathlib/CategoryTheory/Triangulated/Opposite/Pretriangulated.lean

Modified Mathlib/Data/Int/GCD.lean

Modified Mathlib/Data/List/SplitOn.lean

Modified Mathlib/FieldTheory/PrimeField.lean

Modified Mathlib/Geometry/Convex/Cone/TensorProduct.lean

Modified Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean

Modified Mathlib/GroupTheory/Perm/ClosureSwap.lean

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

Modified Mathlib/NumberTheory/ClassNumber/Finite.lean

Modified Mathlib/NumberTheory/RamificationInertia/Basic.lean

Modified Mathlib/NumberTheory/RamificationInertia/Galois.lean

Modified Mathlib/Order/BourbakiWitt.lean

Modified Mathlib/Probability/Process/Stopping.lean

Modified Mathlib/RingTheory/PowerSeries/Trunc.lean

Modified Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean

Modified Mathlib/Topology/Algebra/IsUniformGroup/Defs.lean

Modified Mathlib/Topology/Algebra/Module/PointwiseConvergence.lean

Modified Mathlib/Topology/Semicontinuous.lean