Commit 2023-10-04 14:04 c93575a3

View on Github →

chore: cleanup some spaces (#7484) Purely cosmetic PR.

Estimated changes

Modified Archive/Sensitivity.lean

Modified Mathlib/Algebra/GradedMonoid.lean

Modified Mathlib/AlgebraicTopology/DoldKan/FunctorGamma.lean

Modified Mathlib/AlgebraicTopology/DoldKan/Homotopies.lean

Modified Mathlib/Analysis/Analytic/IsolatedZeros.lean

Modified Mathlib/Analysis/Convex/Segment.lean

Modified Mathlib/CategoryTheory/Abelian/RightDerived.lean

Modified Mathlib/CategoryTheory/Functor/Currying.lean

Modified Mathlib/CategoryTheory/Generator.lean

Modified Mathlib/CategoryTheory/Grothendieck.lean

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

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

Modified Mathlib/CategoryTheory/Localization/Construction.lean

Modified Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean

Modified Mathlib/CategoryTheory/Preadditive/Mat.lean

Modified Mathlib/CategoryTheory/Shift/Basic.lean

Modified Mathlib/CategoryTheory/Shift/Pullback.lean

Modified Mathlib/CategoryTheory/StructuredArrow.lean

Modified Mathlib/Combinatorics/HalesJewett.lean

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean

Modified Mathlib/Data/Finset/Pointwise.lean

Modified Mathlib/Data/List/Basic.lean

Modified Mathlib/Data/PNat/Factors.lean

Modified Mathlib/Data/Part.lean

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

Modified Mathlib/GroupTheory/QuotientGroup.lean

modified theorem QuotientGroup.lift_mk'

modified theorem QuotientGroup.lift_mk

modified theorem QuotientGroup.mk_div

modified theorem QuotientGroup.mk_inv

modified theorem QuotientGroup.mk_mul

modified theorem QuotientGroup.mk_one

modified theorem QuotientGroup.mk_pow

modified theorem QuotientGroup.mk_zpow

Modified Mathlib/LinearAlgebra/AffineSpace/Independent.lean

Modified Mathlib/LinearAlgebra/Basic.lean

Modified Mathlib/LinearAlgebra/Dual.lean

Modified Mathlib/Mathport/Notation.lean

Modified Mathlib/MeasureTheory/Integral/Bochner.lean

Modified Mathlib/ModelTheory/Algebra/Ring/Basic.lean

Modified Mathlib/NumberTheory/KummerDedekind.lean

Modified Mathlib/NumberTheory/LegendreSymbol/Basic.lean

Modified Mathlib/NumberTheory/NumberField/Units.lean

modified theorem NumberField.Units.dirichletUnitTheorem.exists_unit

Modified Mathlib/RingTheory/AdjoinRoot.lean

Modified Mathlib/RingTheory/Discriminant.lean

Modified Mathlib/RingTheory/Henselian.lean

Modified Mathlib/RingTheory/Localization/FractionRing.lean

Modified Mathlib/RingTheory/Nullstellensatz.lean

Modified Mathlib/RingTheory/Perfection.lean

Modified Mathlib/RingTheory/WittVector/Basic.lean

Modified Mathlib/Tactic/ByContra.lean

Modified Mathlib/Tactic/NoncommRing.lean

Modified Mathlib/Topology/ContinuousFunction/Ideals.lean

Modified test/linarith.lean