Commit 2025-04-30 12:59 78ec36cd

View on Github →

chore: more whitespace fixes (#24472) Found by the upcoming linter in #24465.

Estimated changes

Modified Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean

modified theorem AlgHom.eqOn_adjoin_iff

Modified Mathlib/Algebra/BigOperators/Finsupp/Basic.lean

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

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

Modified Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean

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

Modified Mathlib/Algebra/Homology/BifunctorAssociator.lean

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

Modified Mathlib/Algebra/Homology/LocalCohomology.lean

modified def localCohomology.isoSelfLERadical

Modified Mathlib/Algebra/Homology/Localization.lean

Modified Mathlib/Algebra/Homology/Square.lean

Modified Mathlib/Algebra/Module/LocalizedModule/AtPrime.lean

Modified Mathlib/Algebra/Module/LocalizedModule/Away.lean

Modified Mathlib/Algebra/Order/Hom/Basic.lean

Modified Mathlib/Algebra/Quaternion.lean

modified def QuaternionAlgebra.equivProd

modified def QuaternionAlgebra.equivTuple

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

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

Modified Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean

modified def SimplexCategory.factor_δ

modified def SimplexCategory.mkOfLe

Modified Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean

modified def SSet.stdSimplex.const

modified def SSet.stdSimplex.edge

modified def SSet.stdSimplex.triangle

Modified Mathlib/CategoryTheory/Bicategory/Functor/Lax.lean

modified structure CategoryTheory.LaxFunctor

Modified Mathlib/CategoryTheory/Comma/Over/Pullback.lean

Modified Mathlib/CategoryTheory/Grothendieck.lean

modified def CategoryTheory.Grothendieck.functor

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

Modified Mathlib/CategoryTheory/Monoidal/Subcategory.lean

modified theorem CategoryTheory.ObjectProperty.ihom_map

Modified Mathlib/CategoryTheory/ObjectProperty/FullSubcategory.lean

modified theorem CategoryTheory.ObjectProperty.FullSubcategory.lift_comp_inclusion_eq

Modified Mathlib/CategoryTheory/Shift/Opposite.lean

Modified Mathlib/Combinatorics/Enumerative/Composition.lean

modified theorem Composition.sigma_eq_iff_blocks_eq

Modified Mathlib/Condensed/TopCatAdjunction.lean

modified def CondensedSet.compactlyGeneratedAdjunctionCounitHomeo

Modified Mathlib/Condensed/TopComparison.lean

Modified Mathlib/Data/ENNReal/Inv.lean

modified def ENNReal.mulLeftOrderIso

modified def ENNReal.mulRightOrderIso

Modified Mathlib/Data/Finset/Lattice/Fold.lean

Modified Mathlib/Data/Finsupp/Basic.lean

modified def Finsupp.splitSupport

Modified Mathlib/Data/Matrix/Basis.lean

Modified Mathlib/Data/Matrix/Invertible.lean

modified theorem Matrix.invOf_add_mul_mul

modified def Matrix.invertibleAddMulMul

Modified Mathlib/Data/Real/Sqrt.lean

Modified Mathlib/Data/W/Basic.lean

modified def WType.elim

Modified Mathlib/FieldTheory/Minpoly/IsConjRoot.lean

modified theorem IsConjRoot.trans

Modified Mathlib/GroupTheory/NoncommPiCoprod.lean

Modified Mathlib/GroupTheory/Perm/Sign.lean

modified def Equiv.Perm.signBijAux

Modified Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean

Modified Mathlib/LinearAlgebra/Finsupp/VectorSpace.lean

modified theorem Basis.repr_smul'

Modified Mathlib/LinearAlgebra/FreeModule/Basic.lean

modified theorem Module.free_def

Modified Mathlib/Order/WellFoundedSet.lean

Modified Mathlib/RingTheory/Derivation/ToSquareZero.lean

modified def derivationToSquareZeroOfLift

modified def liftOfDerivationToSquareZero

Modified Mathlib/RingTheory/NonUnitalSubring/Basic.lean

Modified Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean

Modified Mathlib/RingTheory/Polynomial/Eisenstein/Criterion.lean

Modified Mathlib/Tactic/Linarith/Lemmas.lean

modified theorem Linarith.sub_neg_of_lt

Modified Mathlib/Topology/Category/CompHausLike/Limits.lean

modified def CompHausLike.isTerminalPUnit

Modified Mathlib/Topology/Category/TopCat/Limits/Basic.lean

modified def TopCat.coconeOfCoconeForget

Modified Mathlib/Topology/Constructions/SumProd.lean

Modified Mathlib/Topology/Sheaves/SheafCondition/Sites.lean

modified theorem TopCat.Presheaf.coveringOfPresieve_apply