Commit 2026-01-30 06:41 8464d9af

View on Github →

style: fix whitespace (#34582) and a few related issues. Found by extending the whitespace linter to proof bodies in #30658.

Estimated changes

Modified Counterexamples/MonicNonRegular.lean

Modified Mathlib/Algebra/Order/Field/Basic.lean

Modified Mathlib/AlgebraicTopology/ModelCategory/CofibrantObjectHomotopy.lean

Modified Mathlib/Analysis/Asymptotics/TVS.lean

modified theorem Asymptotics.isThetaTVS_comm

Modified Mathlib/Analysis/Meromorphic/Basic.lean

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/Orthogonality.lean

Modified Mathlib/CategoryTheory/ComposableArrows/Four.lean

Modified Mathlib/CategoryTheory/Sites/Coherent/ExtensiveTopology.lean

Modified Mathlib/Geometry/Euclidean/NinePointCircle.lean

Modified Mathlib/GroupTheory/FreeGroup/Reduce.lean

modified def FreeGroup.reduce

Modified Mathlib/LinearAlgebra/Transvection.lean

Modified Mathlib/MeasureTheory/VectorMeasure/Basic.lean

Modified Mathlib/Probability/Distributions/Gaussian/HasGaussianLaw/Independence.lean

Modified Mathlib/RepresentationTheory/Intertwining.lean

modified theorem Representation.IntertwiningMap.toLinearMap_apply

Modified Mathlib/RepresentationTheory/Subrepresentation.lean

Modified Mathlib/RingTheory/Morita/Matrix.lean

Modified Mathlib/RingTheory/Polynomial/Chebyshev.lean

Modified Mathlib/Tactic/Ring/NamePolyVars.lean

Modified Mathlib/Topology/Category/LightProfinite/Injective.lean

Modified Mathlib/Topology/Order/LeftRightLim.lean

Modified Mathlib/Topology/UniformSpace/Closeds.lean