Mathlib Changelog
v4
Changelog
About
Github
Commit
2026-04-13 12:57
eb13e32d
View on Github →
style: fix whitespace (
#37993
) Found by extending the whitespace linter to proof bodies in
#30658
.
Estimated changes
Modified
Mathlib/Algebra/Algebra/Operations.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Presheaf/ColimitFunctor.lean
Modified
Mathlib/Algebra/Group/Indicator.lean
Modified
Mathlib/Algebra/Group/Units/Defs.lean
Modified
Mathlib/Algebra/GroupWithZero/Range.lean
Modified
Mathlib/Algebra/Homology/DerivedCategory/Ext/ExtClass.lean
Modified
Mathlib/Algebra/Homology/DerivedCategory/Ext/Map.lean
Modified
Mathlib/Algebra/Homology/DerivedCategory/ShortExact.lean
Modified
Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
Modified
Mathlib/Algebra/Homology/HomotopyCategory/MappingCocone.lean
Modified
Mathlib/Algebra/Homology/Refinements.lean
Modified
Mathlib/Algebra/Homology/SpectralObject/Basic.lean
Modified
Mathlib/Algebra/Homology/SpectralObject/Cycles.lean
Modified
Mathlib/Algebra/Homology/SpectralObject/Differentials.lean
Modified
Mathlib/Algebra/Homology/SpectralObject/EpiMono.lean
Modified
Mathlib/Algebra/Homology/SpectralObject/HasSpectralSequence.lean
Modified
Mathlib/Algebra/Homology/SpectralObject/Page.lean
Modified
Mathlib/Algebra/Homology/SpectralObject/SpectralSequence.lean
Modified
Mathlib/Algebra/Lie/Basis.lean
Modified
Mathlib/Algebra/Lie/Derivation/BaseChange.lean
Modified
Mathlib/Algebra/Lie/Graded.lean
Modified
Mathlib/Algebra/Lie/Prod.lean
Modified
Mathlib/Algebra/Lie/SemiDirect.lean
modified
def
LieAlgebra.SemiDirectSum.prod_iso
Modified
Mathlib/Algebra/Order/GroupWithZero/Range.lean
Modified
Mathlib/AlgebraicTopology/SimplicialComplex/Basic.lean
Modified
Mathlib/AlgebraicTopology/SingularSet.lean
Modified
Mathlib/Analysis/Analytic/Order.lean
Modified
Mathlib/Analysis/Asymptotics/Defs.lean
Modified
Mathlib/Analysis/Calculus/Taylor.lean
Modified
Mathlib/Analysis/Convex/SimplicialComplex/AffineIndependentUnion.lean
Modified
Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean
Modified
Mathlib/Analysis/Distribution/SchwartzSpace/Basic.lean
Modified
Mathlib/Analysis/Distribution/Sobolev.lean
Modified
Mathlib/Analysis/InnerProductSpace/Reproducing.lean
Modified
Mathlib/Analysis/Meromorphic/Basic.lean
Modified
Mathlib/Analysis/Meromorphic/NormalForm.lean
Modified
Mathlib/Analysis/Normed/Algebra/Basic.lean
Modified
Mathlib/Analysis/Normed/Algebra/GelfandFormula.lean
Modified
Mathlib/Analysis/Normed/Field/Krasner.lean
Modified
Mathlib/Analysis/Normed/Lp/lpSpace.lean
Modified
Mathlib/Analysis/Normed/Module/PiTensorProduct/ProjectiveSeminorm.lean
modified
theorem
PiTensorProduct.projectiveSeminorm_add_le
Modified
Mathlib/Analysis/Normed/Ring/InfiniteProd.lean
Modified
Mathlib/Analysis/Normed/Ring/WithAbs.lean
Modified
Mathlib/Analysis/Polynomial/MahlerMeasure.lean
Modified
Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
Modified
Mathlib/Analysis/SpecialFunctions/Gamma/Digamma.lean
Modified
Mathlib/Analysis/SumIntegralExpDecay.lean
Modified
Mathlib/CategoryTheory/Abelian/SerreClass/Localization.lean
Modified
Mathlib/CategoryTheory/Adhesive/Basic.lean
Modified
Mathlib/CategoryTheory/Bicategory/FunctorBicategory/Lax.lean
Modified
Mathlib/CategoryTheory/Bicategory/FunctorBicategory/Oplax.lean
Modified
Mathlib/CategoryTheory/Bicategory/Yoneda.lean
Modified
Mathlib/CategoryTheory/Comma/Over/OverClass.lean
Modified
Mathlib/CategoryTheory/Functor/ReflectsIso/Exact.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Images.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
Modified
Mathlib/CategoryTheory/Sites/Point/OfIsCofiltered.lean
Modified
Mathlib/CategoryTheory/Topos/Sheaf.lean
Modified
Mathlib/CategoryTheory/Triangulated/TStructure/ETrunc.lean
Modified
Mathlib/CategoryTheory/Triangulated/TStructure/TruncLEGT.lean
Modified
Mathlib/CategoryTheory/Triangulated/TStructure/TruncLTGE.lean
Modified
Mathlib/Combinatorics/Graph/Basic.lean
Modified
Mathlib/Combinatorics/Graph/Subgraph.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
Modified
Mathlib/Data/Finsupp/Fin.lean
modified
theorem
Finsupp.cons_zero_single_eq_single_succ
Modified
Mathlib/Data/Finsupp/Indicator.lean
Modified
Mathlib/Data/NNReal/Defs.lean
modified
theorem
NNReal.inv_mk
Modified
Mathlib/Data/Nat/Choose/Multinomial.lean
Modified
Mathlib/Data/QPF/Multivariate/Constructions/Fix.lean
Modified
Mathlib/Data/Sum/Basic.lean
Modified
Mathlib/FieldTheory/RatFunc/IntermediateField.lean
Modified
Mathlib/FieldTheory/RatFunc/Luroth.lean
Modified
Mathlib/Geometry/Euclidean/Sphere/Basic.lean
Modified
Mathlib/Geometry/Euclidean/Volume/Measure.lean
Modified
Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean
Modified
Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean
Modified
Mathlib/Geometry/Manifold/VectorBundle/CovariantDerivative/Basic.lean
Modified
Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean
Modified
Mathlib/Geometry/Manifold/VectorBundle/Tensoriality.lean
Modified
Mathlib/Geometry/Manifold/VectorField/LieBracket.lean
Modified
Mathlib/Geometry/Manifold/VectorField/Pullback.lean
Modified
Mathlib/GroupTheory/DoubleCoset.lean
Modified
Mathlib/GroupTheory/FinitelyPresentedGroup.lean
Modified
Mathlib/GroupTheory/FreeGroup/Basic.lean
Modified
Mathlib/GroupTheory/GroupAction/Hom.lean
Modified
Mathlib/LinearAlgebra/AffineSpace/Simplex/Centroid.lean
Modified
Mathlib/LinearAlgebra/Center.lean
Modified
Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean
Modified
Mathlib/LinearAlgebra/FixedSubmodule.lean
Modified
Mathlib/LinearAlgebra/TensorProduct/Decomposition.lean
Modified
Mathlib/MeasureTheory/Function/ConditionalExpectation/LebesgueBochner.lean
Modified
Mathlib/MeasureTheory/Function/ConditionalExpectation/RadonNikodym.lean
Modified
Mathlib/MeasureTheory/Function/ConditionalLExpectation.lean
modified
theorem
MeasureTheory.condLExp_lt_top
modified
theorem
MeasureTheory.condLExp_ne_top
Modified
Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
Modified
Mathlib/MeasureTheory/Integral/Bochner/SumMeasure.lean
Modified
Mathlib/MeasureTheory/Measure/MutuallySingular.lean
Modified
Mathlib/ModelTheory/Topology/Types.lean
Modified
Mathlib/NumberTheory/Chebyshev.lean
Modified
Mathlib/NumberTheory/Divisors.lean
Modified
Mathlib/NumberTheory/FactorisationProperties.lean
modified
theorem
Nat.deficient_three
Modified
Mathlib/NumberTheory/Height/Basic.lean
Modified
Mathlib/NumberTheory/Height/MvPolynomial.lean
Modified
Mathlib/NumberTheory/Modular.lean
Modified
Mathlib/NumberTheory/ModularForms/EisensteinSeries/E2/Summable.lean
Modified
Mathlib/NumberTheory/ModularForms/EisensteinSeries/E2/Transform.lean
modified
def
EisensteinSeries.δ
modified
theorem
EisensteinSeries.δ_eq
Modified
Mathlib/NumberTheory/NumberField/Completion/InfinitePlace.lean
Modified
Mathlib/NumberTheory/NumberField/Cyclotomic/Galois.lean
Modified
Mathlib/NumberTheory/Padics/Complex.lean
Modified
Mathlib/NumberTheory/Padics/WithVal.lean
Modified
Mathlib/NumberTheory/RatFunc/Ostrowski.lean
Modified
Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
Modified
Mathlib/Probability/CentralLimitTheorem.lean
Modified
Mathlib/Probability/Kernel/Representation.lean
Modified
Mathlib/RepresentationTheory/Action.lean
Modified
Mathlib/RepresentationTheory/Coinduced.lean
Modified
Mathlib/RepresentationTheory/Homological/FiniteCyclic.lean
Modified
Mathlib/RepresentationTheory/Homological/Resolution.lean
Modified
Mathlib/RepresentationTheory/Intertwining.lean
Modified
Mathlib/RepresentationTheory/Invariants.lean
Modified
Mathlib/RepresentationTheory/Rep/Basic.lean
Modified
Mathlib/RingTheory/AdicCompletion/Basic.lean
Modified
Mathlib/RingTheory/Derivation/Lie.lean
modified
def
Derivation.couple
Modified
Mathlib/RingTheory/DividedPowerAlgebra/Init.lean
Modified
Mathlib/RingTheory/FormalGroup/Basic.lean
Modified
Mathlib/RingTheory/Ideal/Cotangent.lean
Modified
Mathlib/RingTheory/Invariant/Basic.lean
Modified
Mathlib/RingTheory/LaurentSeries.lean
Modified
Mathlib/RingTheory/Localization/Basic.lean
Modified
Mathlib/RingTheory/MvPowerSeries/Substitution.lean
Modified
Mathlib/RingTheory/PowerSeries/Substitution.lean
modified
theorem
PowerSeries.coeff_one_substInv
modified
theorem
PowerSeries.subst_C
Modified
Mathlib/RingTheory/Teichmuller.lean
Modified
Mathlib/RingTheory/Valuation/Basic.lean
Modified
Mathlib/RingTheory/Valuation/RankOne.lean
Modified
Mathlib/SetTheory/Cardinal/Cofinality.lean
Modified
Mathlib/SetTheory/Ordinal/Basic.lean
modified
theorem
Cardinal.exists_ord_eq_type_lt
Modified
Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
Modified
Mathlib/Topology/Algebra/Module/FiniteDimensionBilinear.lean
Modified
Mathlib/Topology/Algebra/Valued/ValuativeRel.lean
Modified
Mathlib/Topology/Algebra/Valued/ValuedField.lean
Modified
Mathlib/Topology/Algebra/Valued/WithVal.lean
Modified
Mathlib/Topology/Compactness/CountablyCompact.lean
Modified
Mathlib/Topology/Connected/Clopen.lean
Modified
Mathlib/Topology/DenseEmbedding.lean
Modified
Mathlib/Topology/Instances/Rat.lean
Modified
Mathlib/Topology/MetricSpace/Holder.lean
Modified
Mathlib/Topology/Order/LiminfLimsup.lean
Modified
Mathlib/Topology/Sheaves/Abelian.lean
Modified
Mathlib/Topology/Sheaves/AddCommGrpCat.lean
Modified
Mathlib/Topology/Sheaves/LocallySurjective.lean
Modified
Mathlib/Topology/Sheaves/Presheaf.lean
Modified
Mathlib/Topology/Sion.lean