Commit 2025-07-08 11:58 aa6e5002

View on Github →

chore: whitespace fixes in lemmas (#26892) Found by #26706.

Estimated changes

Modified Archive/Imo/Imo2024Q5.lean

modified theorem Imo2024Q5.Path.one_lt_length_cells

Modified Mathlib/Algebra/BigOperators/Group/Multiset/Basic.lean

Modified Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

modified theorem ModuleCat.extendScalarsId_inv_app_apply

Modified Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean

modified theorem ModuleCat.ofHom₂_compr₂

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

modified theorem SemiconjBy.eq_one_iff

Modified Mathlib/Algebra/GroupWithZero/WithZero.lean

Modified Mathlib/Algebra/Homology/Bifunctor.lean

modified theorem HomologicalComplex.mapBifunctor.d₁_eq_zero

modified theorem HomologicalComplex.mapBifunctor.d₂_eq_zero

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

modified theorem CategoryTheory.ShortComplex.Exact.isIso_toCycles

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

modified theorem CategoryTheory.ShortComplex.fromOpcycles_op_cyclesOpIso_inv

Modified Mathlib/Algebra/Module/Presentation/DirectSum.lean

modified theorem Module.Presentation.directSum_var

Modified Mathlib/Algebra/Quaternion.lean

modified theorem QuaternionAlgebra.coe_ofNat

Modified Mathlib/AlgebraicGeometry/Stalk.lean

modified theorem AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_Spec

Modified Mathlib/AlgebraicTopology/SimplicialSet/CategoryWithFibrations.lean

modified theorem SSet.modelCategoryQuillen.horn_ι_mem_J

Modified Mathlib/Analysis/Calculus/ContDiff/Defs.lean

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Cotangent.lean

modified theorem HasProdUniformlyOn_sineTerm_prod_on_compact

modified theorem Summable_cotTerm

modified theorem cot_series_rep'

modified theorem cot_series_rep

modified theorem logDeriv_sin_div_eq_cot

modified theorem logDeriv_sineTerm_eq_cotTerm

modified theorem sin_pi_z_ne_zero

modified theorem tendsto_logDeriv_euler_cot_sub

modified theorem tendsto_logDeriv_euler_sin_div

Modified Mathlib/CategoryTheory/Bicategory/Adjunction/Mate.lean

Modified Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Pseudo.lean

modified theorem CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_hom

modified theorem CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_inv

Modified Mathlib/CategoryTheory/Closed/Enrichment.lean

modified theorem CategoryTheory.MonoidalClosed.enrichedOrdinaryCategorySelf_homEquiv_symm

Modified Mathlib/CategoryTheory/GradedObject/Braiding.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullback/Categorical/CatCospanTransform.lean

modified theorem CategoryTheory.Limits.CatCospanTransform.hom_ext

Modified Mathlib/CategoryTheory/Limits/Types/ColimitType.lean

Modified Mathlib/CategoryTheory/Localization/SmallHom.lean

modified theorem CategoryTheory.Localization.hasSmallLocalizedHom_iff_target

Modified Mathlib/CategoryTheory/Monoidal/DayConvolution.lean

Modified Mathlib/CategoryTheory/Sites/DenseSubsite/Basic.lean

modified theorem CategoryTheory.Functor.functorPushforward_mem_iff

Modified Mathlib/CategoryTheory/Triangulated/Opposite/Functor.lean

modified theorem CategoryTheory.Functor.op_commShiftIso_hom_app

modified theorem CategoryTheory.Functor.op_commShiftIso_inv_app

Modified Mathlib/Combinatorics/SimpleGraph/Turan.lean

modified theorem SimpleGraph.exists_isTuranMaximal

Modified Mathlib/Data/ENNReal/Operations.lean

modified theorem ENNReal.add_sInf

Modified Mathlib/Data/Sym/Sym2.lean

modified theorem Sym2.map_pmap

Modified Mathlib/Data/Vector/Defs.lean

modified theorem List.Vector.append_def

Modified Mathlib/Geometry/Manifold/ContMDiff/Basic.lean

modified theorem contMDiffOn_iUnion_iff_of_isOpen

Modified Mathlib/Geometry/Manifold/Instances/Icc.lean

modified theorem contMDiff_subtype_coe_Icc

Modified Mathlib/LinearAlgebra/Dimension/Torsion/Finite.lean

deleted theorem rank_eq_zero_iff_isTorsion:

added theorem rank_eq_zero_iff_isTorsion

Modified Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean

modified theorem TensorProduct.directSumRight_comp_rTensor

Modified Mathlib/LinearAlgebra/Multilinear/Curry.lean

modified theorem MultilinearMap.currySum_smul

Modified Mathlib/LinearAlgebra/RootSystem/Base.lean

modified theorem RootPairing.Base.pairingIn_le_zero_of_ne

Modified Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Lemmas.lean

modified theorem RootPairing.Base.root_sub_mem_iff_root_add_mem

Modified Mathlib/LinearAlgebra/RootSystem/RootPositive.lean

modified theorem RootPairing.InvariantForm.apply_root_root_zero_iff

Modified Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Real.lean

Modified Mathlib/NumberTheory/LSeries/Injectivity.lean

modified theorem LSeries.tendsto_atTop

Modified Mathlib/Order/Filter/Basic.lean

modified theorem Filter.EventuallyEq.mul_left

modified theorem Filter.EventuallyEq.mul_right

Modified Mathlib/Order/KrullDimension.lean

modified theorem Order.coe_lt_coheight_iff

Modified Mathlib/Order/Shrink.lean

modified theorem equivShrink_bot

Modified Mathlib/Order/TransfiniteIteration.lean

modified theorem transfiniteIterate_succ

Modified Mathlib/Probability/Kernel/Composition/Lemmas.lean

modified theorem ProbabilityTheory.Kernel.parallelComp_comm

Modified Mathlib/RepresentationTheory/FiniteIndex.lean

modified theorem Rep.coindResAdjunction_counit_app

Modified Mathlib/RingTheory/FilteredAlgebra/Basic.lean

Modified Mathlib/RingTheory/NoetherNormalization.lean

Modified Mathlib/RingTheory/Polynomial/HilbertPoly.lean

modified theorem Polynomial.preHilbertPoly_eq_choose_sub_add

Modified Mathlib/RingTheory/Spectrum/Prime/FreeLocus.lean

modified theorem Module.rankAtStalk_eq_finrank_tensorProduct

Modified Mathlib/RingTheory/TwoSidedIdeal/Operations.lean

modified theorem TwoSidedIdeal.set_mul_subset

modified theorem TwoSidedIdeal.subset_mul_set

Modified Mathlib/Topology/MetricSpace/Congruence.lean

Modified Mathlib/Topology/MetricSpace/UniformConvergence.lean

modified theorem UniformOnFun.edist_eval_le