Commit 2023-09-14 13:42 084cfb35

View on Github →

style: fix wrapping of where (#7149)

Estimated changes

Modified Mathlib/Algebra/Algebra/Equiv.lean

Modified Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

Modified Mathlib/Algebra/Category/GroupCat/Limits.lean

Modified Mathlib/Algebra/Category/GroupCat/ZModuleEquivalence.lean

Modified Mathlib/Algebra/Category/GroupWithZeroCat.lean

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

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

Modified Mathlib/Algebra/DirectSum/Module.lean

Modified Mathlib/Algebra/GradedMonoid.lean

Modified Mathlib/Algebra/GradedMulAction.lean

Modified Mathlib/Algebra/Homology/Additive.lean

Modified Mathlib/Algebra/Homology/HomologicalComplex.lean

modified def HomologicalComplex.comp

Modified Mathlib/Algebra/Homology/LocalCohomology.lean

Modified Mathlib/Algebra/Lie/Basic.lean

Modified Mathlib/Algebra/Lie/Free.lean

Modified Mathlib/Algebra/Lie/Subalgebra.lean

Modified Mathlib/Algebra/Module/Equiv.lean

Modified Mathlib/Algebra/Module/GradedModule.lean

Modified Mathlib/Algebra/Module/LinearMap.lean

Modified Mathlib/Algebra/Module/Submodule/Pointwise.lean

Modified Mathlib/Algebra/Order/Nonneg/Ring.lean

Modified Mathlib/Algebra/Quaternion.lean

Modified Mathlib/Algebra/Star/Pi.lean

Modified Mathlib/Algebra/Star/Prod.lean

Modified Mathlib/Algebra/Star/Unitary.lean

Modified Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.lean

modified def AlgebraicTopology.inclusionOfMooreComplex

Modified Mathlib/Analysis/Complex/Circle.lean

modified def expMapCircle

Modified Mathlib/Analysis/Convex/Body.lean

Modified Mathlib/Analysis/InnerProductSpace/Basic.lean

Modified Mathlib/Analysis/InnerProductSpace/l2Space.lean

Modified Mathlib/Analysis/Normed/Group/AddTorsor.lean

Modified Mathlib/Analysis/Seminorm.lean

Modified Mathlib/CategoryTheory/Abelian/Subobject.lean

Modified Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean

Modified Mathlib/CategoryTheory/Arrow.lean

Modified Mathlib/CategoryTheory/Closed/Monoidal.lean

Modified Mathlib/CategoryTheory/ConcreteCategory/BundledHom.lean

Modified Mathlib/CategoryTheory/EpiMono.lean

modified def CategoryTheory.SplitEpi.splitMono

modified def CategoryTheory.SplitMono.splitEpi

Modified Mathlib/CategoryTheory/Functor/Const.lean

Modified Mathlib/CategoryTheory/Functor/EpiMono.lean

Modified Mathlib/CategoryTheory/Functor/ReflectsIso.lean

Modified Mathlib/CategoryTheory/Idempotents/FunctorCategories.lean

modified def CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.map

Modified Mathlib/CategoryTheory/IsConnected.lean

Modified Mathlib/CategoryTheory/Limits/Connected.lean

modified def CategoryTheory.ProdPreservesConnectedLimits.γ₁

Modified Mathlib/CategoryTheory/Limits/Creates.lean

Modified Mathlib/CategoryTheory/Limits/Final.lean

Modified Mathlib/CategoryTheory/Limits/FullSubcategory.lean

Modified Mathlib/CategoryTheory/Limits/FunctorCategory.lean

Modified Mathlib/CategoryTheory/Limits/Opposites.lean

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

modified def CategoryTheory.Limits.fullyFaithfulReflectsColimits

modified def CategoryTheory.Limits.fullyFaithfulReflectsLimits

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

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

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

modified def CategoryTheory.Limits.perservesColimitsOp

modified def CategoryTheory.Limits.preservesColimitsLeftOp

modified def CategoryTheory.Limits.preservesColimitsRightOp

modified def CategoryTheory.Limits.preservesColimitsUnop

modified def CategoryTheory.Limits.preservesFiniteColimitsOp

modified def CategoryTheory.Limits.preservesFiniteLimitsOp

modified def CategoryTheory.Limits.preservesLimitOp

modified def CategoryTheory.Limits.preservesLimitsLeftOp

modified def CategoryTheory.Limits.preservesLimitsOp

modified def CategoryTheory.Limits.preservesLimitsRightOp

modified def CategoryTheory.Limits.preservesLimitsUnop

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

Modified Mathlib/CategoryTheory/Limits/Preserves/Shapes/Kernels.lean

Modified Mathlib/CategoryTheory/Limits/Preserves/Shapes/Terminal.lean

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

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

Modified Mathlib/CategoryTheory/Limits/Yoneda.lean

Modified Mathlib/CategoryTheory/Monad/Algebra.lean

Modified Mathlib/CategoryTheory/Monad/Limits.lean

Modified Mathlib/CategoryTheory/Monad/Monadicity.lean

Modified Mathlib/CategoryTheory/Monoidal/FunctorCategory.lean

Modified Mathlib/CategoryTheory/Monoidal/NaturalTransformation.lean

Modified Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean

modified def CategoryTheory.closedOfHasLeftDual

Modified Mathlib/CategoryTheory/Over.lean

Modified Mathlib/CategoryTheory/Preadditive/AdditiveFunctor.lean

Modified Mathlib/CategoryTheory/Preadditive/Mat.lean

Modified Mathlib/CategoryTheory/Quotient.lean

Modified Mathlib/CategoryTheory/Sites/Grothendieck.lean

Modified Mathlib/CategoryTheory/Sites/Subsheaf.lean

modified def CategoryTheory.GrothendieckTopology.Subpresheaf.homOfLe

Modified Mathlib/CategoryTheory/Skeletal.lean

modified def CategoryTheory.ThinSkeleton.mapNatTrans

Modified Mathlib/CategoryTheory/Subobject/Comma.lean

Modified Mathlib/CategoryTheory/Types.lean

Modified Mathlib/Combinatorics/Young/YoungDiagram.lean

Modified Mathlib/Control/Bifunctor.lean

Modified Mathlib/Data/Complex/Module.lean

Modified Mathlib/Data/DFinsupp/Basic.lean

Modified Mathlib/Data/Finset/Basic.lean

Modified Mathlib/Data/Finsupp/Basic.lean

Modified Mathlib/Data/Finsupp/Defs.lean

Modified Mathlib/FieldTheory/Adjoin.lean

Modified Mathlib/FieldTheory/Galois.lean

Modified Mathlib/GroupTheory/Congruence.lean

Modified Mathlib/GroupTheory/Coprod.lean

Modified Mathlib/GroupTheory/CoprodI.lean

Modified Mathlib/GroupTheory/GroupAction/ConjAct.lean

Modified Mathlib/GroupTheory/GroupAction/SubMulAction.lean

Modified Mathlib/GroupTheory/GroupAction/SubMulAction/Pointwise.lean

Modified Mathlib/GroupTheory/Subgroup/Basic.lean

Modified Mathlib/GroupTheory/Submonoid/Center.lean

Modified Mathlib/Init/Order/Defs.lean

Modified Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean

Modified Mathlib/LinearAlgebra/Orientation.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/Basic.lean

Modified Mathlib/LinearAlgebra/Quotient.lean

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

Modified Mathlib/MeasureTheory/Constructions/Prod/Basic.lean

Modified Mathlib/MeasureTheory/Measure/FiniteMeasure.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

Modified Mathlib/Order/Category/FinBddDistLatCat.lean

Modified Mathlib/Order/Category/FinBoolAlgCat.lean

Modified Mathlib/Order/Category/NonemptyFinLinOrdCat.lean

Modified Mathlib/Order/Category/PreordCat.lean

Modified Mathlib/Order/Filter/Basic.lean

Modified Mathlib/RepresentationTheory/FdRep.lean

Modified Mathlib/RingTheory/Derivation/Basic.lean

Modified Mathlib/RingTheory/HahnSeries.lean

Modified Mathlib/RingTheory/Ideal/LocalRing.lean

Modified Mathlib/RingTheory/Ideal/Operations.lean

Modified Mathlib/RingTheory/PowerSeries/Basic.lean

Modified Mathlib/RingTheory/PrincipalIdealDomain.lean

Modified Mathlib/Topology/Algebra/ConstMulAction.lean

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

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

Modified Mathlib/Topology/Algebra/Star.lean

Modified Mathlib/Topology/Category/CompHaus/Basic.lean

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

Modified Mathlib/Topology/ContinuousFunction/Ordered.lean

Modified Mathlib/Topology/ContinuousFunction/StoneWeierstrass.lean

modified def ContinuousMap.attachBound

Modified Mathlib/Topology/ContinuousFunction/Units.lean

Modified Mathlib/Topology/Order/Lattice.lean

Modified Mathlib/Topology/SubsetProperties.lean

Modified Mathlib/Topology/VectorBundle/Hom.lean