Commit 2025-04-30 12:59 ad93d6e6

View on Github →

style: further whitespace fixes (#24467) Found by the upcoming linter in #24465.

Estimated changes

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

Modified Mathlib/Algebra/Star/Subsemiring.lean

modified def StarSubsemiring.center

Modified Mathlib/Algebra/Vertex/HVertexOperator.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/Horn.lean

modified def SSet.horn.edge

modified def SSet.horn.edge₃

modified def SSet.horn.face

modified def SSet.horn.primitiveEdge

modified def SSet.horn.primitiveTriangle

Modified Mathlib/Analysis/Analytic/Linear.lean

modified theorem analyticAt_fst

Modified Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean

Modified Mathlib/Analysis/Convex/Body.lean

modified theorem ConvexBody.zero_mem_of_symmetric

Modified Mathlib/Analysis/Fourier/FourierTransformDeriv.lean

Modified Mathlib/Analysis/MellinTransform.lean

Modified Mathlib/Analysis/Normed/Field/WithAbs.lean

modified theorem AbsoluteValue.Completion.locallyCompactSpace

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

Modified Mathlib/CategoryTheory/Category/ReflQuiv.lean

modified def CategoryTheory.ReflQuiv.isoOfEquiv

Modified Mathlib/CategoryTheory/ChosenFiniteProducts/Cat.lean

modified def CategoryTheory.Cat.prodCone

Modified Mathlib/CategoryTheory/ConnectedComponents.lean

modified def CategoryTheory.ConnectedComponents.functorToDiscrete

modified def CategoryTheory.ConnectedComponents.liftFunctor

Modified Mathlib/CategoryTheory/FiberedCategory/Fibered.lean

Modified Mathlib/CategoryTheory/Localization/Pi.lean

Modified Mathlib/CategoryTheory/WithTerminal/Basic.lean

modified def CategoryTheory.WithInitial.mkCommaMorphism

modified def CategoryTheory.WithInitial.ofCommaMorphism

modified def CategoryTheory.WithTerminal.mkCommaMorphism

modified def CategoryTheory.WithTerminal.ofCommaMorphism

Modified Mathlib/Combinatorics/SimpleGraph/Clique.lean

modified theorem SimpleGraph.isIndepSet_neighborSet_of_triangleFree

Modified Mathlib/Data/MLList/BestFirst.lean

Modified Mathlib/Data/Matroid/IndepAxioms.lean

Modified Mathlib/FieldTheory/Minpoly/IsConjRoot.lean

modified theorem IsConjRoot.exists_algEquiv

Modified Mathlib/FieldTheory/Normal/Basic.lean

modified theorem minpoly.exists_algEquiv_of_root'

Modified Mathlib/Geometry/Manifold/Algebra/Structures.lean

modified theorem topologicalSemiring_of_contMDiffRing

Modified Mathlib/Geometry/Manifold/ChartedSpace.lean

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

Modified Mathlib/GroupTheory/GroupExtension/Basic.lean

Modified Mathlib/GroupTheory/GroupExtension/Defs.lean

Modified Mathlib/GroupTheory/SemidirectProduct.lean

Modified Mathlib/LinearAlgebra/FreeProduct/Basic.lean

modified theorem DirectSum.induction_lon

Modified Mathlib/LinearAlgebra/Matrix/Spectrum.lean

Modified Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean

Modified Mathlib/MeasureTheory/Group/MeasurableEquiv.lean

Modified Mathlib/MeasureTheory/Integral/Asymptotics.lean

Modified Mathlib/MeasureTheory/Integral/MeanInequalities.lean

Modified Mathlib/MeasureTheory/MeasurableSpace/Constructions.lean

modified theorem measurable_update'

Modified Mathlib/MeasureTheory/MeasurableSpace/EventuallyMeasurable.lean

modified def EventuallyMeasurableSet

Modified Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean

modified theorem Basis.parallelepiped_eq_map

Modified Mathlib/MeasureTheory/Measure/Regular.lean

Modified Mathlib/Order/LiminfLimsup.lean

Modified Mathlib/Topology/Algebra/Category/ProfiniteGrp/Basic.lean

modified def ProfiniteGrp.ofClosedSubgroup

Modified Mathlib/Topology/Algebra/OpenSubgroup.lean

modified theorem Subgroup.isOpen_of_one_mem_interior

Modified Mathlib/Topology/Algebra/Valued/WithVal.lean

Modified Mathlib/Topology/ContinuousMap/Algebra.lean

Modified Mathlib/Topology/ContinuousMap/Bounded/Normed.lean

Modified Mathlib/Topology/LocallyConstant/Algebra.lean

modified def LocallyConstant.comapMonoidHom

Modified Mathlib/Topology/MetricSpace/Dilation.lean

Modified Mathlib/Topology/MetricSpace/Gluing.lean

modified def Metric.inductiveLimitDist

modified theorem Metric.inductiveLimitDist_eq_dist

Modified Mathlib/Topology/Sheaves/SheafCondition/Sites.lean

modified def TopCat.Presheaf.presieveOfCovering.indexOfHom

modified theorem TopCat.Presheaf.presieveOfCovering.indexOfHom_spec