Commit 2025-07-09 14:52 18a0fbd0

View on Github →

chore: fix whitespaces (#26930) Found by #26926.

Estimated changes

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean

modified theorem MeasureTheory.eLpNorm_condExp_le

Modified Mathlib/RingTheory/MvPowerSeries/Substitution.lean

Modified Mathlib/RingTheory/NoetherNormalization.lean

Modified Mathlib/RingTheory/OrderOfVanishing.lean

Modified Mathlib/RingTheory/Polynomial/ContentIdeal.lean

Modified Mathlib/RingTheory/Polynomial/DegreeLT.lean

Modified Mathlib/RingTheory/Polynomial/HilbertPoly.lean

Modified Mathlib/RingTheory/Polynomial/ShiftedLegendre.lean

Modified Mathlib/RingTheory/PolynomialLaw/Basic.lean

Modified Mathlib/RingTheory/PowerSeries/Derivative.lean

Modified Mathlib/RingTheory/PowerSeries/Substitution.lean

Modified Mathlib/RingTheory/QuotSMulTop.lean

modified def QuotSMulTop.map

Modified Mathlib/RingTheory/WittVector/Basic.lean

Modified Mathlib/RingTheory/WittVector/Frobenius.lean

Modified Mathlib/RingTheory/WittVector/Identities.lean

Modified Mathlib/RingTheory/WittVector/WittPolynomial.lean

Modified Mathlib/SetTheory/Descriptive/Tree.lean

Modified Mathlib/SetTheory/Game/Birthday.lean

Modified Mathlib/SetTheory/Game/Ordinal.lean

Modified Mathlib/SetTheory/Lists.lean

Modified Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean

Modified Mathlib/SetTheory/Ordinal/NaturalOps.lean

Modified Mathlib/SetTheory/Ordinal/Notation.lean

Modified Mathlib/SetTheory/PGame/Basic.lean

Modified Mathlib/SetTheory/Surreal/Multiplication.lean

Modified Mathlib/SetTheory/ZFC/Class.lean

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

Modified Mathlib/Topology/Baire/BaireMeasurable.lean

Modified Mathlib/Topology/CWComplex/Classical/Basic.lean

Modified Mathlib/Topology/Category/Compactum.lean

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

Modified Mathlib/Topology/Category/Profinite/Nobeling/Span.lean

Modified Mathlib/Topology/Category/Profinite/Nobeling/Successor.lean

Modified Mathlib/Topology/Category/Profinite/Nobeling/ZeroLimit.lean

Modified Mathlib/Topology/Homotopy/Lifting.lean

modified theorem IsCoveringMap.exists_path_lifts

Modified Mathlib/Topology/Instances/CantorSet.lean

modified theorem quarter_mem_cantorSet

modified theorem quarter_mem_preCantorSet

modified theorem quarters_mem_preCantorSet

Modified Mathlib/Topology/MetricSpace/BundledFun.lean

Modified Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean

Modified Mathlib/Topology/MetricSpace/HolderNorm.lean

Modified Mathlib/Topology/Order/LowerUpperTopology.lean

Modified Mathlib/Topology/Order/ScottTopology.lean

modified theorem Topology.scottHausdorff_le_scott

Modified Mathlib/Topology/Sheaves/MayerVietoris.lean

Modified Mathlib/Topology/Sheaves/Skyscraper.lean

Modified Mathlib/Topology/UniformSpace/OfCompactT2.lean