Commit 2023-10-30 15:05 24cd315a

View on Github →

chore: remove some double spaces (#7983)

Estimated changes

Modified Mathlib/Algebra/Algebra/Equiv.lean

Modified Mathlib/Algebra/Algebra/Opposite.lean

Modified Mathlib/Algebra/ContinuedFractions/Translations.lean

Modified Mathlib/Algebra/GradedMulAction.lean

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

modified def CochainComplex.shiftFunctorAdd'

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

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

Modified Mathlib/AlgebraicTopology/DoldKan/EquivalencePseudoabelian.lean

modified def CategoryTheory.Idempotents.DoldKan.N

modified def CategoryTheory.Idempotents.DoldKan.Γ

Modified Mathlib/Analysis/NormedSpace/OperatorNorm.lean

Modified Mathlib/CategoryTheory/Limits/Preserves/Basic.lean

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

modified def CategoryTheory.Limits.biprod.associator

Modified Mathlib/CategoryTheory/Monoidal/Skeleton.lean

Modified Mathlib/CategoryTheory/Shift/Induced.lean

Modified Mathlib/CategoryTheory/Sites/IsSheafFor.lean

Modified Mathlib/CategoryTheory/Yoneda.lean

modified theorem CategoryTheory.yonedaEquiv_comp'

modified theorem CategoryTheory.yonedaEquiv_comp

Modified Mathlib/Combinatorics/SetFamily/Compression/UV.lean

Modified Mathlib/Data/Complex/Basic.lean

modified theorem Complex.ofReal_bit0

Modified Mathlib/Data/Finset/LocallyFinite.lean

Modified Mathlib/FieldTheory/Subfield.lean

modified theorem Subfield.coe_subtype

Modified Mathlib/GroupTheory/OrderOfElement.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat.lean

modified theorem QuadraticModuleCat.toIsometry_id

Modified Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean

modified theorem QuadraticForm.associated_baseChange

modified theorem QuadraticForm.polarBilin_baseChange

Modified Mathlib/MeasureTheory/Integral/Layercake.lean

Modified Mathlib/MeasureTheory/Measure/FiniteMeasure.lean

modified theorem MeasureTheory.FiniteMeasure.map_add

modified theorem MeasureTheory.FiniteMeasure.map_smul

Modified Mathlib/NumberTheory/NumberField/Units.lean

modified theorem NumberField.Units.dirichletUnitTheorem.exists_unit

Modified Mathlib/Order/Filter/Germ.lean

Modified Mathlib/Probability/Independence/Basic.lean

modified theorem ProbabilityTheory.Indep_iff

modified theorem ProbabilityTheory.Indep_iff_IndepSets

Modified Mathlib/Tactic/MkIffOfInductiveProp.lean

Modified Mathlib/Tactic/NormNum/OfScientific.lean

Modified Mathlib/Tactic/ToAdditive.lean

Modified Mathlib/Tactic/Widget/Calc.lean

Modified Mathlib/Testing/SlimCheck/Testable.lean

Modified Mathlib/Topology/Clopen.lean

Modified Mathlib/Topology/Connected/Basic.lean

Modified Mathlib/Topology/NoetherianSpace.lean

Modified scripts/fix-by-linebreaks.sh

Modified test/Real.lean