Commit 2023-10-04 08:36 39a866a8

View on Github →

chore: cleanup some spaces (#7490) Purely cosmetic PR

Estimated changes

Modified Archive/Sensitivity.lean

Modified Mathlib/Algebra/Category/MonCat/FilteredColimits.lean

Modified Mathlib/Algebra/GeomSum.lean

Modified Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean

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

modified theorem CategoryTheory.ShortComplex.exact_op_iff

Modified Mathlib/Algebra/Ring/Aut.lean

modified def RingAut.toPerm

Modified Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean

Modified Mathlib/Data/Holor.lean

Modified Mathlib/Data/List/Sigma.lean

Modified Mathlib/Data/Nat/GCD/Basic.lean

modified theorem Nat.coprime_sub_self_right

Modified Mathlib/Data/Nat/PartENat.lean

modified theorem PartENat.coe_succ_le_iff

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

Modified Mathlib/Data/Rat/Lemmas.lean

Modified Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean

Modified Mathlib/GroupTheory/MonoidLocalization.lean

Modified Mathlib/LinearAlgebra/TensorProduct.lean

Modified Mathlib/MeasureTheory/Decomposition/UnsignedHahn.lean

Modified Mathlib/MeasureTheory/Integral/Bochner.lean

Modified Mathlib/NumberTheory/ArithmeticFunction.lean

Modified Mathlib/Order/Partition/Finpartition.lean

Modified Mathlib/RingTheory/IsAdjoinRoot.lean

Modified Mathlib/RingTheory/Norm.lean

Modified Mathlib/RingTheory/Valuation/Integers.lean

Modified Mathlib/SetTheory/Ordinal/Notation.lean

Modified Mathlib/Tactic/NormNum/Inv.lean

modified def Mathlib.Meta.NormNum.evalMkRat

Modified Mathlib/Topology/Algebra/InfiniteSum/Basic.lean

Modified Mathlib/Topology/Order/UpperLowerSetTopology.lean

Modified test/push_neg.lean