Commit 2024-07-13 01:16 8cf527bf

View on Github →

style: fix some double spaces (#14662) All remaining occurrences of : are about manually aligning things. This PR also found a few instances where this alignment was broken, and either removes the double spaces or restores the alignment.

Estimated changes

Modified Mathlib/Algebra/Algebra/NonUnitalHom.lean

Modified Mathlib/Algebra/Algebra/Operations.lean

Modified Mathlib/Algebra/Homology/HomologicalComplex.lean

Modified Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean

Modified Mathlib/Algebra/Module/LocalizedModule.lean

Modified Mathlib/Analysis/NormedSpace/PiTensorProduct/InjectiveSeminorm.lean

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

modified theorem CategoryTheory.Limits.sequentialFunctor_map

Modified Mathlib/Combinatorics/SetFamily/FourFunctions.lean

modified theorem collapse_of_mem

Modified Mathlib/Computability/Encoding.lean

Modified Mathlib/Data/Nat/SuccPred.lean

Modified Mathlib/GroupTheory/PushoutI.lean

Modified Mathlib/MeasureTheory/Integral/Bochner.lean

Modified Mathlib/RingTheory/FreeCommRing.lean

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

Modified Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean

modified theorem OrdinalApprox.gfp_mem_range_gfpApprox

Modified Mathlib/Tactic/FunProp/Theorems.lean

Modified Mathlib/Tactic/FunProp/Types.lean

Modified Mathlib/Tactic/Linarith/Frontend.lean

Modified Mathlib/Tactic/NormNum/Core.lean

Modified Mathlib/Topology/Category/Stonean/Limits.lean

modified def Stonean.pullback.isLimit