Commit 2025-03-12 08:26 c26a1a17

View on Github →

chore(whitespace): more changes (#22853) Found by #22760.

Estimated changes

Modified Mathlib/Analysis/Analytic/Linear.lean

modified theorem analyticWithinAt_fst

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

Modified Mathlib/Analysis/Convex/Segment.lean

Modified Mathlib/Analysis/Normed/Lp/PiLp.lean

modified theorem WithLp.equiv_symm_pi_apply

Modified Mathlib/Analysis/Normed/Lp/lpSpace.lean

modified theorem lp.singleContinuousLinearMap_apply

Modified Mathlib/Analysis/Normed/Unbundled/FiniteExtension.lean

Modified Mathlib/Condensed/AB.lean

Modified Mathlib/Condensed/Discrete/Basic.lean

Modified Mathlib/Condensed/Discrete/LocallyConstant.lean

modified def CompHausLike.LocallyConstant.unit

Modified Mathlib/Condensed/Epi.lean

Modified Mathlib/Condensed/Explicit.lean

Modified Mathlib/Condensed/Light/Epi.lean

Modified Mathlib/Condensed/Limits.lean

Modified Mathlib/Condensed/Module.lean

Modified Mathlib/Condensed/Solid.lean

Modified Mathlib/Data/PFunctor/Univariate/M.lean

Modified Mathlib/Data/TypeVec.lean

modified theorem TypeVec.appendFun_comp

Modified Mathlib/GroupTheory/CoprodI.lean

Modified Mathlib/LinearAlgebra/Multilinear/DFinsupp.lean

Modified Mathlib/MeasureTheory/Group/Defs.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean

Modified Mathlib/ModelTheory/Algebra/Field/IsAlgClosed.lean

modified theorem FirstOrder.Field.lift_genericMonicPoly

Modified Mathlib/NumberTheory/RamificationInertia/Basic.lean

Modified Mathlib/Probability/Independence/Conditional.lean

modified theorem ProbabilityTheory.CondIndepSets.union_iff

Modified Mathlib/RingTheory/Binomial.lean

Modified Mathlib/Topology/Algebra/Module/Multilinear/Basic.lean

Modified Mathlib/Topology/Category/LightProfinite/Basic.lean