Commit 2026-01-13 18:40 65982bbc

View on Github →

style: fix whitespace (#33899) Found by extending the whitespace linter to proof bodies in #30658 and #33393.

Estimated changes

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

Modified Mathlib/Algebra/Lie/Weights/IsSimple.lean

Modified Mathlib/AlgebraicGeometry/Modules/Tilde.lean

Modified Mathlib/AlgebraicTopology/SimplicialObject/Split.lean

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Continuity.lean

Modified Mathlib/Analysis/InnerProductSpace/l2Space.lean

Modified Mathlib/Analysis/Normed/Algebra/Spectrum.lean

Modified Mathlib/Analysis/RCLike/Basic.lean

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

Modified Mathlib/CategoryTheory/Bicategory/Adjunction/Mate.lean

Modified Mathlib/CategoryTheory/Bicategory/Extension.lean

Modified Mathlib/CategoryTheory/Functor/Derived/Adjunction.lean

Modified Mathlib/CategoryTheory/Join/Opposites.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Opposites/Equalizers.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullback/Cospan.lean

Modified Mathlib/CategoryTheory/Monoidal/Braided/Transport.lean

Modified Mathlib/CategoryTheory/Monoidal/Cartesian/Grp_.lean

Modified Mathlib/CategoryTheory/MorphismProperty/FunctorCategory.lean

Modified Mathlib/CategoryTheory/Presentable/Directed.lean

Modified Mathlib/CategoryTheory/Shift/Induced.lean

Modified Mathlib/CategoryTheory/Shift/Opposite.lean

Modified Mathlib/CategoryTheory/Sites/Sieves.lean

Modified Mathlib/CategoryTheory/Sites/Types.lean

Modified Mathlib/CategoryTheory/Triangulated/Adjunction.lean

Modified Mathlib/CategoryTheory/WithTerminal/Basic.lean

Modified Mathlib/Combinatorics/Additive/ApproximateSubgroup.lean

Modified Mathlib/Combinatorics/Matroid/Dual.lean

Modified Mathlib/Combinatorics/Matroid/Sum.lean

Modified Mathlib/Data/Fin/Tuple/Embedding.lean

modified def Function.Embedding.twoEmbeddingEquiv

Modified Mathlib/Data/Int/Bitwise.lean

Modified Mathlib/FieldTheory/Differential/Basic.lean

Modified Mathlib/Geometry/Manifold/Riemannian/Basic.lean

Modified Mathlib/GroupTheory/SpecificGroups/Dihedral.lean

Modified Mathlib/LinearAlgebra/Alternating/Basic.lean

Modified Mathlib/LinearAlgebra/Finsupp/Pi.lean

Modified Mathlib/MeasureTheory/Integral/Layercake.lean

Modified Mathlib/NumberTheory/Dioph.lean

Modified Mathlib/NumberTheory/LucasLehmer.lean

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/PolarCoord.lean

Modified Mathlib/NumberTheory/NumberField/FinitePlaces.lean

Modified Mathlib/NumberTheory/Padics/PadicNumbers.lean

Modified Mathlib/Order/Hom/Basic.lean

Modified Mathlib/RepresentationTheory/Rep.lean

Modified Mathlib/RingTheory/Ideal/Quotient/Operations.lean

Modified Mathlib/RingTheory/Morita/Matrix.lean

Modified Mathlib/RingTheory/PicardGroup.lean

Modified Mathlib/RingTheory/Polynomial/Eisenstein/Criterion.lean

Modified Mathlib/RingTheory/Valuation/ValuationSubring.lean

Modified Mathlib/Topology/VectorBundle/Riemannian.lean