Commit 2025-12-17 10:18 cfa7d94f

View on Github →

chore: tidy various files (#32981) As usual, simps didn't look noticeably slow.

Estimated changes

Modified Mathlib/AlgebraicTopology/FundamentalGroupoid/SimplyConnected.lean

Modified Mathlib/Analysis/Calculus/ContDiff/Bounds.lean

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

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

Modified Mathlib/Analysis/Convex/Quasiconvex.lean

Modified Mathlib/Analysis/Distribution/DerivNotation.lean

Modified Mathlib/Analysis/Distribution/Distribution.lean

Modified Mathlib/Analysis/Normed/Lp/SmoothApprox.lean

Modified Mathlib/Analysis/SpecialFunctions/Arcosh.lean

Modified Mathlib/Analysis/SpecialFunctions/Elliptic/Weierstrass.lean

modified theorem PeriodPair.weierstrassP_bound

Modified Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean

Modified Mathlib/CategoryTheory/Localization/SmallShiftedHom.lean

Modified Mathlib/CategoryTheory/Shift/CommShiftTwo.lean

Modified Mathlib/CategoryTheory/Yoneda.lean

Modified Mathlib/Data/Finsupp/Option.lean

Modified Mathlib/Data/Int/Fib/Basic.lean

Modified Mathlib/Data/List/PeriodicityLemma.lean

Modified Mathlib/Data/List/Sort.lean

Modified Mathlib/Data/Sym/Card.lean

Modified Mathlib/LinearAlgebra/AffineSpace/Independent.lean

Modified Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean

Modified Mathlib/LinearAlgebra/Matrix/Irreducible/Defs.lean

Modified Mathlib/LinearAlgebra/Matrix/PosDef.lean

Modified Mathlib/LinearAlgebra/Multilinear/Basis.lean

Modified Mathlib/LinearAlgebra/SpecialLinearGroup.lean

Modified Mathlib/LinearAlgebra/SymmetricAlgebra/Basic.lean

Modified Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean