Commit 2025-08-31 15:32 0f063cda

View on Github →

chore: tidy various files (#29148)

Estimated changes

Modified Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

Modified Mathlib/Algebra/Group/Finsupp.lean

Modified Mathlib/AlgebraicGeometry/Modules/Tilde.lean

Modified Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean

Modified Mathlib/Analysis/LocallyConvex/WithSeminorms.lean

Modified Mathlib/Analysis/Normed/Group/AddCircle.lean

Modified Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/IntegralRepresentation.lean

Modified Mathlib/CategoryTheory/Adjunction/Evaluation.lean

Modified Mathlib/CategoryTheory/Comma/Over/Basic.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/DisjointCoproduct.lean

Modified Mathlib/CategoryTheory/Monad/Algebra.lean

Modified Mathlib/CategoryTheory/Subobject/ArtinianObject.lean

Modified Mathlib/CategoryTheory/Subobject/MonoOver.lean

Modified Mathlib/Combinatorics/SimpleGraph/Clique.lean

Modified Mathlib/Combinatorics/SimpleGraph/Coloring.lean

Modified Mathlib/Combinatorics/SimpleGraph/Extremal/Turan.lean

modified theorem SimpleGraph.turanGraph_adj

Modified Mathlib/Data/Fin/Embedding.lean

Modified Mathlib/Data/Matrix/Mul.lean

Modified Mathlib/LinearAlgebra/Eigenspace/Matrix.lean

Modified Mathlib/LinearAlgebra/Matrix/ToLin.lean

Modified Mathlib/MeasureTheory/Measure/Support.lean

Modified Mathlib/NumberTheory/TsumDivsorsAntidiagonal.lean

modified def divisorsAntidiagonalFactors

Modified Mathlib/Order/KrullDimension.lean

Modified Mathlib/Probability/Independence/Basic.lean

Modified Mathlib/Probability/Martingale/Basic.lean

Modified Mathlib/RepresentationTheory/Basic.lean

Modified Mathlib/RingTheory/HahnSeries/Addition.lean

Modified Mathlib/RingTheory/HahnSeries/HEval.lean

Modified Mathlib/RingTheory/Ideal/Maps.lean

Modified Mathlib/RingTheory/IsAdjoinRoot.lean

Modified Mathlib/RingTheory/LaurentSeries.lean

Modified Mathlib/RingTheory/MvPolynomial/Symmetric/Defs.lean

Modified Mathlib/Tactic/NormNum/Basic.lean