Commit 2025-03-13 02:38 2edf64c8

View on Github →

chore: whitespace again (#22878) Found by #22760.

Estimated changes

Modified Mathlib/Algebra/Module/ZLattice/Basic.lean

Modified Mathlib/Algebra/Module/ZLattice/Covolume.lean

Modified Mathlib/Analysis/Analytic/Uniqueness.lean

modified theorem Asymptotics.IsBigO.continuousMultilinearMap_apply_eq_zero

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

modified def OrderedFinpartition.applyOrderedFinpartition

modified theorem OrderedFinpartition.applyOrderedFinpartition_apply

modified theorem OrderedFinpartition.applyOrderedFinpartition_update_left

modified theorem OrderedFinpartition.norm_applyOrderedFinpartition_le

Modified Mathlib/Analysis/Calculus/LogDeriv.lean

Modified Mathlib/Analysis/Fourier/FourierTransformDeriv.lean

Modified Mathlib/Analysis/InnerProductSpace/PiL2.lean

Modified Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean

modified theorem ContinuousMultilinearMap.norm_restr

modified def ContinuousMultilinearMap.restr

Modified Mathlib/Analysis/NormedSpace/Multilinear/Curry.lean

modified theorem ContinuousMultilinearMap.apply_zero_uncurry0

modified theorem ContinuousMultilinearMap.curry0_apply

modified theorem ContinuousMultilinearMap.curry0_norm

modified theorem ContinuousMultilinearMap.curryFinFinset_apply

modified theorem ContinuousMultilinearMap.curryFinFinset_apply_const

modified theorem ContinuousMultilinearMap.fin0_apply_norm

modified def ContinuousMultilinearMap.uncurry0

modified theorem ContinuousMultilinearMap.uncurry0_curry0

modified def continuousMultilinearCurryFin0

modified theorem continuousMultilinearCurryFin0_apply

modified def continuousMultilinearCurryFin1

modified theorem continuousMultilinearCurryFin1_apply

modified def continuousMultilinearCurryRightEquiv'

Modified Mathlib/Condensed/Discrete/Characterization.lean

modified theorem CondensedMod.isDiscrete_tfae

modified theorem CondensedSet.isDiscrete_tfae

modified theorem LightCondMod.isDiscrete_tfae

modified theorem LightCondSet.isDiscrete_tfae

Modified Mathlib/Geometry/Manifold/Algebra/Monoid.lean

modified theorem mdifferentiableAt_mul_right

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

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

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

Modified Mathlib/MeasureTheory/Integral/SetIntegral.lean

Modified Mathlib/MeasureTheory/Measure/Haar/Quotient.lean