Commit 2025-03-02 11:36 39688c3a

View on Github →

chore: tidy various files (#22442)

Estimated changes

Modified Mathlib/Algebra/Module/ZLattice/Basic.lean

Modified Mathlib/Algebra/Order/Antidiag/Nat.lean

Modified Mathlib/Algebra/Polynomial/Laurent.lean

Modified Mathlib/Algebra/Polynomial/Roots.lean

Modified Mathlib/Algebra/Polynomial/Sequence.lean

Modified Mathlib/Analysis/Asymptotics/ExpGrowth.lean

Modified Mathlib/Analysis/BoxIntegral/UnitPartition.lean

Modified Mathlib/Analysis/InnerProductSpace/Basic.lean

Modified Mathlib/CategoryTheory/Abelian/FreydMitchell.lean

Modified Mathlib/CategoryTheory/Abelian/Indization.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Preorder/WellOrderContinuous.lean

Modified Mathlib/Data/Matroid/Circuit.lean

Modified Mathlib/Data/Matroid/Closure.lean

Modified Mathlib/Data/Matroid/Loop.lean

Modified Mathlib/Data/Set/Card/Arithmetic.lean

Modified Mathlib/Geometry/Manifold/ChartedSpace.lean

Modified Mathlib/Geometry/Manifold/ContMDiff/Constructions.lean

Modified Mathlib/Logic/Denumerable.lean

Modified Mathlib/MeasureTheory/Measure/LogLikelihoodRatio.lean

Modified Mathlib/NumberTheory/Padics/MahlerBasis.lean

Modified Mathlib/Probability/Kernel/Composition/MeasureComp.lean

Modified Mathlib/Probability/Moments/Basic.lean

Modified Mathlib/RingTheory/Artinian/Ring.lean

Modified Mathlib/RingTheory/Generators.lean

Modified Mathlib/RingTheory/MvPowerSeries/Trunc.lean

Modified Mathlib/RingTheory/NoetherNormalization.lean

Modified Mathlib/Topology/Algebra/ContinuousMonoidHom.lean

modified def ContinuousMulEquiv.trans

Modified Mathlib/Topology/Basic.lean

Modified scripts/nolints_prime_decls.txt