Commit 2025-04-08 20:01 f63a9a65

View on Github →

chore: tidy various files (#23821)

Estimated changes

Modified Archive/Imo/Imo1998Q2.lean

Modified Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean

Modified Mathlib/Algebra/Category/Ring/Limits.lean

Modified Mathlib/Algebra/Exact.lean

Modified Mathlib/Algebra/Group/ForwardDiff.lean

modified def fwdDiff_aux.fwdDiffₗ

Modified Mathlib/Algebra/Group/Idempotent.lean

modified theorem IsIdempotentElem.iff_eq_one_of_isUnit

Modified Mathlib/Algebra/Module/SnakeLemma.lean

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

Modified Mathlib/Algebra/Polynomial/CoeffList.lean

Modified Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean

Modified Mathlib/Analysis/CStarAlgebra/PositiveLinearMap.lean

Modified Mathlib/Analysis/Convex/EGauge.lean

Modified Mathlib/Analysis/SpecialFunctions/Complex/CircleMap.lean

modified theorem periodic_circleMap

Modified Mathlib/CategoryTheory/MorphismProperty/WeakFactorizationSystem.lean

Modified Mathlib/Combinatorics/Nullstellensatz.lean

Modified Mathlib/Data/Finsupp/Defs.lean

Modified Mathlib/Data/Finsupp/Single.lean

Modified Mathlib/Data/Int/WithZero.lean

Modified Mathlib/Data/Matroid/Minor/Basic.lean

Modified Mathlib/Data/SetLike/Basic.lean

Modified Mathlib/FieldTheory/JacobsonNoether.lean

Modified Mathlib/Geometry/Euclidean/Sphere/Tangent.lean

Modified Mathlib/GroupTheory/FreeGroup/Basic.lean

Modified Mathlib/NumberTheory/LSeries/Linearity.lean

Modified Mathlib/NumberTheory/LSeries/PrimesInAP.lean

Modified Mathlib/NumberTheory/Padics/RingHoms.lean

Modified Mathlib/Order/IsNormal.lean

Modified Mathlib/Order/KrullDimension.lean

Modified Mathlib/RingTheory/AlgebraicIndependent/Basic.lean

Modified Mathlib/RingTheory/Length.lean

Modified Mathlib/RingTheory/LocalProperties/Projective.lean

Modified Mathlib/RingTheory/MvPowerSeries/Basic.lean

Modified Mathlib/RingTheory/Nilpotent/Exp.lean

Modified Mathlib/RingTheory/PolynomialLaw/Basic.lean

Modified Mathlib/RingTheory/Spectrum/Prime/Topology.lean

Modified Mathlib/RingTheory/Valuation/LocalSubring.lean

Modified Mathlib/Topology/Compactness/DeltaGeneratedSpace.lean

Modified Mathlib/Topology/Constructible.lean