Commit 2025-05-01 02:12 203067e9

View on Github →

chore: whitespace adaptations (#24488) Found by #24465.

Estimated changes

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

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

Modified Mathlib/Algebra/Order/Floor/Defs.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Basic.lean

modified theorem HasFDerivWithinAt.of_nhdsWithin_eq_bot

Modified Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean

modified theorem MeasureTheory.eLpNorm_le_eLpNorm_fderiv_of_eq_inner

modified theorem MeasureTheory.eLpNorm_le_eLpNorm_fderiv_one

Modified Mathlib/CategoryTheory/Monoidal/Subcategory.lean

Modified Mathlib/Computability/Language.lean

Modified Mathlib/Condensed/TopCatAdjunction.lean

modified def CondensedSet.condensedSetToCompactlyGenerated

modified def CondensedSet.topCatAdjunctionCounit

modified def CondensedSet.topCatAdjunctionCounitEquiv

modified theorem CondensedSet.topCatAdjunctionCounit_bijective

modified def condensedSetToTopCat

Modified Mathlib/RingTheory/Ideal/IsPrincipalPowQuotient.lean

modified def Ideal.quotEquivPowQuotPowSuccEquiv