Mathlib Changelog
v4
Changelog
About
Github
Commit
2026-03-01 08:33
338973d7
View on Github →
chore: fix whitespace (
#35909
) Found by extending the whitespace linter to proof bodies in
#30658
.
Estimated changes
Modified
Mathlib/Algebra/Category/ModuleCat/Stalk.lean
Modified
Mathlib/Algebra/Homology/SpectralSequence/Basic.lean
Modified
Mathlib/Algebra/Lie/SemiDirect.lean
Modified
Mathlib/Algebra/Module/SpanRank.lean
Modified
Mathlib/AlgebraicGeometry/ColimitsOver.lean
Modified
Mathlib/AlgebraicGeometry/Group/Abelian.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/QuasiFinite.lean
Modified
Mathlib/AlgebraicGeometry/Normalization.lean
Modified
Mathlib/AlgebraicGeometry/Restrict.lean
Modified
Mathlib/AlgebraicGeometry/Spec.lean
Modified
Mathlib/AlgebraicGeometry/StructureSheaf.lean
Modified
Mathlib/AlgebraicGeometry/ZariskisMainTheorem.lean
Modified
Mathlib/AlgebraicTopology/ModelCategory/BifibrantObjectHomotopy.lean
Modified
Mathlib/AlgebraicTopology/ModelCategory/FibrantObjectHomotopy.lean
Modified
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean
Modified
Mathlib/Analysis/Complex/Periodic.lean
Modified
Mathlib/Analysis/Complex/Poisson.lean
Modified
Mathlib/Analysis/Convex/Approximation.lean
Modified
Mathlib/Analysis/InnerProductSpace/Harmonic/HarmonicContOnCl.lean
Modified
Mathlib/Analysis/Normed/Group/Bounded.lean
Modified
Mathlib/Analysis/Normed/Operator/Banach.lean
Modified
Mathlib/Analysis/Normed/Ring/Basic.lean
Modified
Mathlib/CategoryTheory/Limits/FunctorCategory/BinaryBiproducts.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Pullback/PullbackObjObj.lean
Modified
Mathlib/CategoryTheory/Monoidal/Cartesian/Grp_.lean
Modified
Mathlib/CategoryTheory/RegularCategory/Basic.lean
Modified
Mathlib/CategoryTheory/Sites/DenseSubsite/OneHypercoverDense.lean
Modified
Mathlib/CategoryTheory/Sites/Descent/DescentDataPrime.lean
Modified
Mathlib/CategoryTheory/Triangulated/TStructure/AbelianSubcategory.lean
Modified
Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
Modified
Mathlib/GroupTheory/Focal.lean
modified
theorem
Subgroup.commutator_inf_eq_focalSubgroup
Modified
Mathlib/GroupTheory/GroupAction/OfQuotient.lean
Modified
Mathlib/InformationTheory/Coding/KraftMcMillan.lean
Modified
Mathlib/LinearAlgebra/Matrix/Stochastic.lean
Modified
Mathlib/MeasureTheory/Function/ConditionalLExpectation.lean
Modified
Mathlib/MeasureTheory/Function/LpSeminorm/LpNorm.lean
Modified
Mathlib/MeasureTheory/Integral/IntervalIntegral/AbsolutelyContinuousFun.lean
Modified
Mathlib/MeasureTheory/VectorMeasure/BoundedVariation.lean
Modified
Mathlib/NumberTheory/ModularForms/DedekindEta.lean
Modified
Mathlib/NumberTheory/RamificationInertia/HilbertTheory.lean
Modified
Mathlib/Order/ConditionallyCompletePartialOrder/Defs.lean
Modified
Mathlib/Order/ScottContinuity.lean
Modified
Mathlib/Order/Types/Arithmetic.lean
Modified
Mathlib/Order/Types/Defs.lean
Modified
Mathlib/RepresentationTheory/Irreducible.lean
Modified
Mathlib/RingTheory/Etale/QuasiFinite.lean
Modified
Mathlib/RingTheory/Ideal/AssociatedPrime/Basic.lean
Modified
Mathlib/RingTheory/Localization/AtPrime/Basic.lean
Modified
Mathlib/RingTheory/QuasiFinite/Weakly.lean
Modified
Mathlib/RingTheory/Smooth/IntegralClosure.lean
Modified
Mathlib/RingTheory/TensorProduct/IncludeLeftSubRight.lean
Modified
Mathlib/RingTheory/Unramified/LocalStructure.lean
Modified
Mathlib/RingTheory/ZariskisMainTheorem.lean
Modified
Mathlib/SetTheory/Ordinal/Notation.lean
Modified
Mathlib/Tactic/CategoryTheory/Coherence/Datatypes.lean
Modified
Mathlib/Tactic/Module.lean
Modified
Mathlib/Topology/Algebra/Module/ClosedSubmodule.lean
Modified
Mathlib/Topology/Algebra/Monoid/Defs.lean
Modified
Mathlib/Topology/Algebra/RestrictedProduct/Basic.lean
Modified
Mathlib/Topology/Algebra/RestrictedProduct/Units.lean
Modified
Mathlib/Topology/ContinuousMap/ContinuousMapZero.lean
modified
theorem
ContinuousMapZero.continuous_postcomp
Modified
Mathlib/Topology/Irreducible.lean
Modified
Mathlib/Topology/LocallyFinsupp.lean