Commit 2023-11-09 12:45 c488ddff

View on Github →

style: add missing spaces around colons (#8293) This is not exhaustive

Estimated changes

Modified Mathlib/Algebra/Group/TypeTags.lean

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

modified def CategoryTheory.ShortComplex.FunctorEquivalence.counitIso

Modified Mathlib/Algebra/PUnitInstances.lean

Modified Mathlib/Analysis/NormedSpace/lpSpace.lean

Modified Mathlib/CategoryTheory/Monad/Monadicity.lean

Modified Mathlib/CategoryTheory/Monoidal/Category.lean

modified theorem CategoryTheory.MonoidalCategory.tensorHom_def'

Modified Mathlib/Combinatorics/Partition.lean

Modified Mathlib/Data/List/MinMax.lean

Modified Mathlib/Data/Nat/Digits.lean

modified theorem Nat.sum_le_ofDigits

Modified Mathlib/Data/Nat/PartENat.lean

modified theorem PartENat.get_ofNat'

Modified Mathlib/Data/Ordmap/Ordnode.lean

Modified Mathlib/Data/QPF/Multivariate/Constructions/Cofix.lean

modified theorem MvQPF.liftR_map_last

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

Modified Mathlib/Init/Algebra/Classes.lean

Modified Mathlib/Order/Basic.lean

Modified Mathlib/RingTheory/Derivation/Lie.lean

Modified Mathlib/RingTheory/Flat.lean

Modified Mathlib/RingTheory/PowerSeries/Derivative.lean

Modified Mathlib/RingTheory/TensorProduct.lean

modified theorem Algebra.TensorProduct.map_id

Modified Mathlib/SetTheory/Ordinal/NaturalOps.lean

Modified Mathlib/Tactic/Linarith/Preprocessing.lean

modified def Linarith.isNatCoe

Modified Mathlib/Topology/Category/Profinite/Nobeling.lean

modified theorem Profinite.NobelingProof.Products.isGood_nil

Modified Mathlib/Topology/LocallyConstant/Algebra.lean

modified def LocallyConstant.comapₐ

modified def LocallyConstant.congrLeftₐ

modified def LocallyConstant.congrLeftₗ