Skip to content

Comments

chore: add H1 headers#35324

Draft
harahu wants to merge 1 commit intoleanprover-community:masterfrom
harahu:chore/add-headers
Draft

chore: add H1 headers#35324
harahu wants to merge 1 commit intoleanprover-community:masterfrom
harahu:chore/add-headers

Conversation

@harahu
Copy link
Contributor

@harahu harahu commented Feb 14, 2026 •
edited
Loading

This PR introduces a script that identifies lean files that don't have an H1 header.

I've added a placeholder header to the identified files and will use this branch to develop smaller PRs.

Open in Gitpod

@harahu
Copy link
Contributor Author

harahu commented Feb 14, 2026

WIP

@github-actions github-actions bot added the WIP Work in progress label Feb 14, 2026
@github-actions
Copy link

github-actions bot commented Feb 14, 2026

PR summary 88bb6d226a

Import changes for modified files

Dependency changes

File Base Count Head Count Change
Mathlib.Algebra.Algebra.Subalgebra.IsSimpleOrder 1402 0 -1402 (-100.00%)
Mathlib.Algebra.AlgebraicCard 1355 0 -1355 (-100.00%)
Mathlib.Algebra.ArithmeticGeometric 1224 0 -1224 (-100.00%)
Mathlib.Algebra.Category.Grp.FiniteGrp 501 0 -501 (-100.00%)
Mathlib.Algebra.Category.Grp.ZModuleEquivalence 763 0 -763 (-100.00%)
Mathlib.Algebra.Category.ModuleCat.Adjunctions 1183 0 -1183 (-100.00%)
Mathlib.Algebra.CharP.Frobenius 910 0 -910 (-100.00%)
Mathlib.Algebra.GroupWithZero.Int 248 0 -248 (-100.00%)
Mathlib.Algebra.Homology.ComplexShapeSigns 1017 0 -1017 (-100.00%)
Mathlib.Algebra.Homology.HomologicalComplexBiprod 778 0 -778 (-100.00%)
Mathlib.Algebra.Homology.HomotopyCategory.HomComplex 1216 0 -1216 (-100.00%)
Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift 1260 0 -1260 (-100.00%)
Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor 1309 0 -1309 (-100.00%)
Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated 1273 0 -1273 (-100.00%)
Mathlib.Algebra.Homology.HomotopyCategory.Triangulated 1274 0 -1274 (-100.00%)
Mathlib.Algebra.Homology.HomotopyCofiber 967 0 -967 (-100.00%)
Mathlib.Algebra.Homology.Localization 986 0 -986 (-100.00%)
Mathlib.Algebra.Homology.TotalComplexSymmetry 1109 0 -1109 (-100.00%)
Mathlib.Algebra.Lie.CartanMatrix 580 0 -580 (-100.00%)
Mathlib.Algebra.ModEq 251 0 -251 (-100.00%)
Mathlib.Algebra.Module.Submodule.Equiv 656 0 -656 (-100.00%)
Mathlib.Algebra.MvPolynomial.Counit 1041 0 -1041 (-100.00%)
Mathlib.Algebra.MvPolynomial.Expand 1362 0 -1362 (-100.00%)
Mathlib.Algebra.NoZeroSMulDivisors.Prod 248 0 -248 (-100.00%)
Mathlib.Algebra.Order.Archimedean.Hom 654 0 -654 (-100.00%)
Mathlib.Algebra.Order.Field.Defs 60 0 -60 (-100.00%)
Mathlib.Algebra.Order.Interval.Set.Group 293 0 -293 (-100.00%)
Mathlib.Algebra.Order.Module.Algebra 526 0 -526 (-100.00%)
Mathlib.Algebra.Order.Monoid.ToMulBot 407 0 -407 (-100.00%)
Mathlib.Algebra.Order.PartialSups 252 0 -252 (-100.00%)
Mathlib.Algebra.Polynomial.Degree.Definitions 904 0 -904 (-100.00%)
Mathlib.Algebra.Polynomial.Factors 580 0 -580 (-100.00%)
Mathlib.Algebra.QuadraticAlgebra 1273 0 -1273 (-100.00%)
Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap 2210 0 -2210 (-100.00%)
Mathlib.AlgebraicTopology.DoldKan.Compatibility 294 0 -294 (-100.00%)
Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive 1104 0 -1104 (-100.00%)
Mathlib.AlgebraicTopology.DoldKan.GammaCompN 1100 0 -1100 (-100.00%)
Mathlib.AlgebraicTopology.DoldKan.NCompGamma 1103 0 -1103 (-100.00%)
Mathlib.AlgebraicTopology.MooreComplex 951 0 -951 (-100.00%)
Mathlib.AlgebraicTopology.SimplexCategory.Augmented 859 0 -859 (-100.00%)
Mathlib.Analysis.Analytic.CPolynomialDef 1694 0 -1694 (-100.00%)
Mathlib.Analysis.Calculus.ContDiff.RestrictScalars 1749 0 -1749 (-100.00%)
Mathlib.Analysis.Calculus.Deriv.Shift 1766 0 -1766 (-100.00%)
Mathlib.Analysis.Calculus.TangentCone 1476 0 -1476 (-100.00%)
Mathlib.Analysis.Distribution.FourierSchwartz 2575 0 -2575 (-100.00%)
Mathlib.Analysis.Distribution.SchwartzSpace 2629 0 -2629 (-100.00%)
Mathlib.Analysis.InnerProductSpace.Harmonic.Analytic 2214 0 -2214 (-100.00%)
Mathlib.Analysis.InnerProductSpace.Projection 2165 0 -2165 (-100.00%)
Mathlib.Analysis.Matrix 2204 0 -2204 (-100.00%)
Mathlib.Analysis.Normed.Field.Ultra 1415 0 -1415 (-100.00%)
Mathlib.Analysis.Normed.Module.ENormedSpace 1081 0 -1081 (-100.00%)
Mathlib.Analysis.NormedSpace.Alternating.Basic 1283 0 -1283 (-100.00%)
Mathlib.Analysis.NormedSpace.Alternating.Curry 1283 0 -1283 (-100.00%)
Mathlib.Analysis.NormedSpace.Alternating.Uncurry.Fin 1286 0 -1286 (-100.00%)
Mathlib.Analysis.NormedSpace.BallAction 1101 0 -1101 (-100.00%)
Mathlib.Analysis.NormedSpace.ConformalLinearMap 1101 0 -1101 (-100.00%)
Mathlib.Analysis.NormedSpace.Connected 1251 0 -1251 (-100.00%)
Mathlib.Analysis.NormedSpace.DualNumber 1753 0 -1753 (-100.00%)
Mathlib.Analysis.NormedSpace.ENormedSpace 1081 0 -1081 (-100.00%)
Mathlib.Analysis.NormedSpace.Extend 1288 0 -1288 (-100.00%)
Mathlib.Analysis.NormedSpace.Extr 1102 0 -1102 (-100.00%)
Mathlib.Analysis.NormedSpace.FunctionSeries 1243 0 -1243 (-100.00%)
Mathlib.Analysis.NormedSpace.HahnBanach.Extension 1381 0 -1381 (-100.00%)
Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual 1376 0 -1376 (-100.00%)
Mathlib.Analysis.NormedSpace.HahnBanach.Separation 1376 0 -1376 (-100.00%)
Mathlib.Analysis.NormedSpace.HomeomorphBall 1282 0 -1282 (-100.00%)
Mathlib.Analysis.NormedSpace.IndicatorFunction 1081 0 -1081 (-100.00%)
Mathlib.Analysis.NormedSpace.Int 1101 0 -1101 (-100.00%)
Mathlib.Analysis.NormedSpace.MStructure 1081 0 -1081 (-100.00%)
Mathlib.Analysis.NormedSpace.Multilinear.Basic 1283 0 -1283 (-100.00%)
Mathlib.Analysis.NormedSpace.Multilinear.Curry 1283 0 -1283 (-100.00%)
Mathlib.Analysis.NormedSpace.MultipliableUniformlyOn 2216 0 -2216 (-100.00%)
Mathlib.Analysis.NormedSpace.Normalize 1282 0 -1282 (-100.00%)
Mathlib.Analysis.NormedSpace.OperatorNorm.Asymptotics 1283 0 -1283 (-100.00%)
Mathlib.Analysis.NormedSpace.OperatorNorm.Basic 1283 0 -1283 (-100.00%)
Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear 1283 0 -1283 (-100.00%)
Mathlib.Analysis.NormedSpace.OperatorNorm.Completeness 1283 0 -1283 (-100.00%)
Mathlib.Analysis.NormedSpace.OperatorNorm.Mul 1283 0 -1283 (-100.00%)
Mathlib.Analysis.NormedSpace.OperatorNorm.NNNorm 1283 0 -1283 (-100.00%)
Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace 1283 0 -1283 (-100.00%)
Mathlib.Analysis.NormedSpace.OperatorNorm.Prod 1283 0 -1283 (-100.00%)
Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm 1283 0 -1283 (-100.00%)
Mathlib.Analysis.NormedSpace.PiTensorProduct.ProjectiveSeminorm 1283 0 -1283 (-100.00%)
Mathlib.Analysis.NormedSpace.Pointwise 1248 0 -1248 (-100.00%)
Mathlib.Analysis.NormedSpace.RCLike 1288 0 -1288 (-100.00%)
Mathlib.Analysis.NormedSpace.Real 1101 0 -1101 (-100.00%)
Mathlib.Analysis.NormedSpace.RieszLemma 1249 0 -1249 (-100.00%)
Mathlib.Analysis.NormedSpace.SphereNormEquiv 1101 0 -1101 (-100.00%)
Mathlib.Analysis.Real.Pi.Leibniz 2524 0 -2524 (-100.00%)
Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog 2317 0 -2317 (-100.00%)
Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev 1571 0 -1571 (-100.00%)
Mathlib.CategoryTheory.Adhesive 843 0 -843 (-100.00%)
Mathlib.CategoryTheory.Adjunction.Whiskering 410 0 -410 (-100.00%)
Mathlib.CategoryTheory.Bicategory.Functor.Strict 251 0 -251 (-100.00%)
Mathlib.CategoryTheory.Bicategory.Strict 298 0 -298 (-100.00%)
Mathlib.CategoryTheory.Category.Grpd 253 0 -253 (-100.00%)
Mathlib.CategoryTheory.Closed.Cartesian 253 0 -253 (-100.00%)
Mathlib.CategoryTheory.Closed.Enrichment 253 0 -253 (-100.00%)
Mathlib.CategoryTheory.Closed.Functor 253 0 -253 (-100.00%)
Mathlib.CategoryTheory.Closed.FunctorCategory.Basic 253 0 -253 (-100.00%)
Mathlib.CategoryTheory.Closed.FunctorCategory.Complete 253 0 -253 (-100.00%)
Mathlib.CategoryTheory.Closed.FunctorCategory.Groupoid 251 0 -251 (-100.00%)
Mathlib.CategoryTheory.Closed.FunctorToTypes 253 0 -253 (-100.00%)
Mathlib.CategoryTheory.Closed.Ideal 253 0 -253 (-100.00%)
Mathlib.CategoryTheory.Closed.Monoidal 251 0 -251 (-100.00%)
Mathlib.CategoryTheory.Closed.Types 253 0 -253 (-100.00%)
Mathlib.CategoryTheory.Closed.Zero 253 0 -253 (-100.00%)
Mathlib.CategoryTheory.ConcreteCategory.BundledHom 249 0 -249 (-100.00%)
Mathlib.CategoryTheory.ConcreteCategory.Elementwise 461 0 -461 (-100.00%)
Mathlib.CategoryTheory.ConcreteCategory.ReflectsIso 409 0 -409 (-100.00%)
Mathlib.CategoryTheory.ConcreteCategory.UnbundledHom 249 0 -249 (-100.00%)
Mathlib.CategoryTheory.EffectiveEpi.RegularEpi 253 0 -253 (-100.00%)
Mathlib.CategoryTheory.Functor.Hom 407 0 -407 (-100.00%)
Mathlib.CategoryTheory.Groupoid.Basic 403 0 -403 (-100.00%)
Mathlib.CategoryTheory.Limits.FormalCoproducts 607 0 -607 (-100.00%)
Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq 253 0 -253 (-100.00%)
Mathlib.CategoryTheory.Limits.Types.Shapes 253 0 -253 (-100.00%)
Mathlib.CategoryTheory.Localization.FiniteProducts 653 0 -653 (-100.00%)
Mathlib.CategoryTheory.Localization.HasLocalization 422 0 -422 (-100.00%)
Mathlib.CategoryTheory.Localization.Monoidal 433 0 -433 (-100.00%)
Mathlib.CategoryTheory.LocallyDirected 433 0 -433 (-100.00%)
Mathlib.CategoryTheory.Monoidal.Limits 458 0 -458 (-100.00%)
Mathlib.CategoryTheory.Preadditive.Yoneda.Injective 1100 0 -1100 (-100.00%)
Mathlib.CategoryTheory.Preadditive.Yoneda.Projective 1099 0 -1099 (-100.00%)
Mathlib.CategoryTheory.Products.Associator 300 0 -300 (-100.00%)
Mathlib.CategoryTheory.Shift.ShiftSequence 699 0 -699 (-100.00%)
Mathlib.CategoryTheory.Shift.ShiftedHom 762 0 -762 (-100.00%)
Mathlib.CategoryTheory.Shift.ShiftedHomOpposite 778 0 -778 (-100.00%)
Mathlib.CategoryTheory.Sites.Adjunction 769 0 -769 (-100.00%)
Mathlib.CategoryTheory.Sites.CompatiblePlus 712 0 -712 (-100.00%)
Mathlib.CategoryTheory.Sites.CompatibleSheafification 727 0 -727 (-100.00%)
Mathlib.CategoryTheory.Sites.CoversTop 710 0 -710 (-100.00%)
Mathlib.CategoryTheory.Sites.Over 1051 0 -1051 (-100.00%)
Mathlib.CategoryTheory.Sites.SheafHom 1052 0 -1052 (-100.00%)
Mathlib.CategoryTheory.Sites.Whiskering 710 0 -710 (-100.00%)
Mathlib.CategoryTheory.Subpresheaf.Basic 251 0 -251 (-100.00%)
Mathlib.CategoryTheory.Subpresheaf.Equalizer 253 0 -253 (-100.00%)
Mathlib.CategoryTheory.Subpresheaf.Finite 253 0 -253 (-100.00%)
Mathlib.CategoryTheory.Subpresheaf.Image 253 0 -253 (-100.00%)
Mathlib.CategoryTheory.Subpresheaf.OfSection 253 0 -253 (-100.00%)
Mathlib.CategoryTheory.Subpresheaf.Sieves 253 0 -253 (-100.00%)
Mathlib.CategoryTheory.Subpresheaf.Subobject 253 0 -253 (-100.00%)
Mathlib.Combinatorics.Enumerative.Partition 712 0 -712 (-100.00%)
Mathlib.Combinatorics.Quiver.ConnectedComponent 129 0 -129 (-100.00%)
Mathlib.Combinatorics.Quiver.Subquiver 114 0 -114 (-100.00%)
Mathlib.Combinatorics.Quiver.Symmetric 125 0 -125 (-100.00%)
Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected 583 0 -583 (-100.00%)
Mathlib.Combinatorics.SimpleGraph.Turan 485 0 -485 (-100.00%)
Mathlib.Combinatorics.SimpleGraph.Walk 483 0 -483 (-100.00%)
Mathlib.Computability.Primrec 602 0 -602 (-100.00%)
Mathlib.Control.Basic 53 0 -53 (-100.00%)
Mathlib.Data.Complex.Cardinality 1224 0 -1224 (-100.00%)
Mathlib.Data.Complex.Exponential 1301 0 -1301 (-100.00%)
Mathlib.Data.Complex.ExponentialBounds 1719 0 -1719 (-100.00%)
Mathlib.Data.Complex.FiniteDimensional 1224 0 -1224 (-100.00%)
Mathlib.Data.Complex.Norm 1277 0 -1277 (-100.00%)
Mathlib.Data.Complex.Order 1282 0 -1282 (-100.00%)
Mathlib.Data.Complex.Trigonometric 1303 0 -1303 (-100.00%)
Mathlib.Data.FinEnum 469 0 -469 (-100.00%)
Mathlib.Data.Finsupp.MonomialOrder.DegLex 935 0 -935 (-100.00%)
Mathlib.Data.Fintype.BigOperators 543 0 -543 (-100.00%)
Mathlib.Data.Fintype.Sum 442 0 -442 (-100.00%)
Mathlib.Data.Int.ConditionallyCompleteOrder 268 0 -268 (-100.00%)
Mathlib.Data.List.Defs 63 0 -63 (-100.00%)
Mathlib.Data.List.Induction 249 0 -249 (-100.00%)
Mathlib.Data.List.InsertNth 248 0 -248 (-100.00%)
Mathlib.Data.List.Lookmap 53 0 -53 (-100.00%)
Mathlib.Data.List.ModifyLast 53 0 -53 (-100.00%)
Mathlib.Data.List.SplitOn 263 0 -263 (-100.00%)
Mathlib.Data.List.TakeWhile 113 0 -113 (-100.00%)
Mathlib.Data.Nat.Choose.Mul 247 0 -247 (-100.00%)
Mathlib.Data.Nat.PowModTotient 1039 0 -1039 (-100.00%)
Mathlib.Data.Nat.Prime.Infinite 366 0 -366 (-100.00%)
Mathlib.Data.Nat.Set 206 0 -206 (-100.00%)
Mathlib.Data.Nat.Size 123 0 -123 (-100.00%)
Mathlib.Data.QPF.Multivariate.Constructions.Prj 514 0 -514 (-100.00%)
Mathlib.Data.Rat.Cast.OfScientific 564 0 -564 (-100.00%)
Mathlib.Data.Rat.NatSqrt.Defs 530 0 -530 (-100.00%)
Mathlib.Data.Rat.NatSqrt.Real 1279 0 -1279 (-100.00%)
Mathlib.Data.Real.Cardinality 1224 0 -1224 (-100.00%)
Mathlib.Data.Real.Hyperreal 1224 0 -1224 (-100.00%)
Mathlib.Data.Real.Irrational 1274 0 -1274 (-100.00%)
Mathlib.Data.Real.Pi.Bounds 1757 0 -1757 (-100.00%)
Mathlib.Data.Real.Pi.Irrational 2216 0 -2216 (-100.00%)
Mathlib.Data.Real.Pi.Leibniz 2216 0 -2216 (-100.00%)
Mathlib.Data.Real.Pi.Wallis 2216 0 -2216 (-100.00%)
Mathlib.Data.Seq.Seq 253 0 -253 (-100.00%)
Mathlib.Data.Tree.RBMap 50 0 -50 (-100.00%)
Mathlib.Data.Vector.Defs 253 0 -253 (-100.00%)
Mathlib.Data.Vector.MapLemmas 371 0 -371 (-100.00%)
Mathlib.Data.Vector.Snoc 370 0 -370 (-100.00%)
Mathlib.Deprecated.Aliases 47 0 -47 (-100.00%)
Mathlib.Deprecated.Order 60 0 -60 (-100.00%)
Mathlib.Deprecated.RingHom 250 0 -250 (-100.00%)
Mathlib.Deprecated.Sort 48 0 -48 (-100.00%)
Mathlib.FieldTheory.Finite.Polynomial 1698 0 -1698 (-100.00%)
Mathlib.Geometry.Manifold.Bordism 2234 0 -2234 (-100.00%)
Mathlib.Geometry.Manifold.ContMDiff.Atlas 2204 0 -2204 (-100.00%)
Mathlib.Geometry.Manifold.ContMDiff.Basic 2203 0 -2203 (-100.00%)
Mathlib.Geometry.Manifold.ContMDiff.Constructions 2204 0 -2204 (-100.00%)
Mathlib.Geometry.Manifold.ContMDiff.NormedSpace 2206 0 -2206 (-100.00%)
Mathlib.Geometry.Manifold.ContMDiffMFDeriv 2231 0 -2231 (-100.00%)
Mathlib.Geometry.Manifold.MFDeriv.FDeriv 2206 0 -2206 (-100.00%)
Mathlib.Geometry.Manifold.MFDeriv.NormedSpace 2213 0 -2213 (-100.00%)
Mathlib.GroupTheory.Commutator.Finite 857 0 -857 (-100.00%)
Mathlib.GroupTheory.FreeGroup.CyclicallyReduced 606 0 -606 (-100.00%)
Mathlib.GroupTheory.FreeGroup.Orbit 467 0 -467 (-100.00%)
Mathlib.GroupTheory.HNNExtension 853 0 -853 (-100.00%)
Mathlib.GroupTheory.PushoutI 854 0 -854 (-100.00%)
Mathlib.Init 46 0 -46 (-100.00%)
Mathlib.Lean.Expr 54 0 -54 (-100.00%)
Mathlib.Lean.GoalsLocation 49 0 -49 (-100.00%)
Mathlib.Lean.Message 49 0 -49 (-100.00%)
Mathlib.Lean.Meta 51 0 -51 (-100.00%)
Mathlib.Lean.Meta.RefinedDiscrTree 56 0 -56 (-100.00%)
Mathlib.LinearAlgebra.AffineSpace.ContinuousAffineEquiv 651 0 -651 (-100.00%)
Mathlib.LinearAlgebra.GeneralLinearGroup 482 0 -482 (-100.00%)
Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus 1912 0 -1912 (-100.00%)
Mathlib.LinearAlgebra.Matrix.LDL 1760 0 -1760 (-100.00%)
Mathlib.LinearAlgebra.Prod 814 0 -814 (-100.00%)
Mathlib.LinearAlgebra.Quotient.Card 794 0 -794 (-100.00%)
Mathlib.LinearAlgebra.SModEq 891 0 -891 (-100.00%)
Mathlib.LinearAlgebra.SesquilinearForm 976 0 -976 (-100.00%)
Mathlib.Logic.Function.FiberPartition 176 0 -176 (-100.00%)
Mathlib.Logic.IsEmpty 89 0 -89 (-100.00%)
Mathlib.Logic.IsEmpty.Basic 88 0 -88 (-100.00%)
Mathlib.NumberTheory.ArithmeticFunction 1739 0 -1739 (-100.00%)
Mathlib.NumberTheory.Cyclotomic.Embeddings 2232 0 -2232 (-100.00%)
Mathlib.NumberTheory.Cyclotomic.PID 2577 0 -2577 (-100.00%)
Mathlib.NumberTheory.Cyclotomic.Rat 2577 0 -2577 (-100.00%)
Mathlib.NumberTheory.Cyclotomic.Three 2577 0 -2577 (-100.00%)
Mathlib.NumberTheory.Harmonic.Bounds 2519 0 -2519 (-100.00%)
Mathlib.NumberTheory.Harmonic.Defs 465 0 -465 (-100.00%)
Mathlib.NumberTheory.Harmonic.Int 1480 0 -1480 (-100.00%)
Mathlib.NumberTheory.NumberField.Completion 2215 0 -2215 (-100.00%)
Mathlib.NumberTheory.TsumDivsorsAntidiagonal 1328 0 -1328 (-100.00%)
Mathlib.NumberTheory.VonMangoldt 1736 0 -1736 (-100.00%)
Mathlib.Order.Quotient 357 0 -357 (-100.00%)
Mathlib.Order.Types.Arithmetic 591 0 -591 (-100.00%)
Mathlib.Probability.Independence.Kernel 1648 0 -1648 (-100.00%)
Mathlib.Probability.Integration 2214 0 -2214 (-100.00%)
Mathlib.RingTheory.DedekindDomain.GaussLemma 2001 0 -2001 (-100.00%)
Mathlib.RingTheory.GradedAlgebra.Radical 1148 0 -1148 (-100.00%)
Mathlib.RingTheory.HopkinsLevitzki 1799 0 -1799 (-100.00%)
Mathlib.RingTheory.Ideal.IdempotentFG 1100 0 -1100 (-100.00%)
Mathlib.RingTheory.LocalRing.Quotient 1485 0 -1485 (-100.00%)
Mathlib.RingTheory.Localization.AtPrime 1208 0 -1208 (-100.00%)
Mathlib.RingTheory.Localization.Away.AdjoinRoot 1608 0 -1608 (-100.00%)
Mathlib.RingTheory.MvPowerSeries.Expand 1631 0 -1631 (-100.00%)
Mathlib.RingTheory.MvPowerSeries.LexOrder 1110 0 -1110 (-100.00%)
Mathlib.RingTheory.PowerSeries.Expand 1640 0 -1640 (-100.00%)
Mathlib.RingTheory.SimpleModule.InjectiveProjective 1231 0 -1231 (-100.00%)
Mathlib.RingTheory.SimpleRing.Matrix 1188 0 -1188 (-100.00%)
Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC 1742 0 -1742 (-100.00%)
Mathlib.RingTheory.Spectrum.Prime.Noetherian 1755 0 -1755 (-100.00%)
Mathlib.RingTheory.Trace.Quotient 2038 0 -2038 (-100.00%)
Mathlib.RingTheory.Valuation.IntegrallyClosed 676 0 -676 (-100.00%)
Mathlib.RingTheory.Valuation.ValuativeRel 1140 0 -1140 (-100.00%)
Mathlib.RingTheory.WittVector.Frobenius 1711 0 -1711 (-100.00%)
Mathlib.RingTheory.WittVector.Identities 1714 0 -1714 (-100.00%)
Mathlib.RingTheory.WittVector.Isocrystal 1764 0 -1764 (-100.00%)
Mathlib.RingTheory.WittVector.MulP 1710 0 -1710 (-100.00%)
Mathlib.RingTheory.WittVector.Verschiebung 1710 0 -1710 (-100.00%)
Mathlib.SetTheory.Ordinal.Topology 904 0 -904 (-100.00%)
Mathlib.SetTheory.Surreal.Multiplication 857 0 -857 (-100.00%)
Mathlib.Tactic 2945 0 -2945 (-100.00%)
Mathlib.Tactic.Algebraize 813 0 -813 (-100.00%)
Mathlib.Tactic.ApplyCongr 47 0 -47 (-100.00%)
Mathlib.Tactic.Bound 528 0 -528 (-100.00%)
Mathlib.Tactic.CancelDenoms 514 0 -514 (-100.00%)
Mathlib.Tactic.CategoryTheory.CheckCompositions 266 0 -266 (-100.00%)
Mathlib.Tactic.Conv 47 0 -47 (-100.00%)
Mathlib.Tactic.DeclarationNames 1 0 -1 (-100.00%)
Mathlib.Tactic.DepRewrite 48 0 -48 (-100.00%)
Mathlib.Tactic.FunProp.Attr 65 0 -65 (-100.00%)
Mathlib.Tactic.FunProp.Decl 47 0 -47 (-100.00%)
Mathlib.Tactic.FunProp.Elab 68 0 -68 (-100.00%)
Mathlib.Tactic.FunProp.FunctionData 53 0 -53 (-100.00%)
Mathlib.Tactic.FunProp.Mor 51 0 -51 (-100.00%)
Mathlib.Tactic.FunProp.Theorems 64 0 -64 (-100.00%)
Mathlib.Tactic.FunProp.ToBatteries 47 0 -47 (-100.00%)
Mathlib.Tactic.FunProp.Types 56 0 -56 (-100.00%)
Mathlib.Tactic.GeneralizeProofs 49 0 -49 (-100.00%)
Mathlib.Tactic.GuardGoalNums 47 0 -47 (-100.00%)
Mathlib.Tactic.GuardHypNums 47 0 -47 (-100.00%)
Mathlib.Tactic.Inhabit 50 0 -50 (-100.00%)
Mathlib.Tactic.Linarith 599 0 -599 (-100.00%)
Mathlib.Tactic.Linter 54 0 -54 (-100.00%)
Mathlib.Tactic.Linter.CommandStart 49 0 -49 (-100.00%)
Mathlib.Tactic.Linter.TextBased 50 0 -50 (-100.00%)
Mathlib.Tactic.Linter.UnusedTacticExtension 1 0 -1 (-100.00%)
Mathlib.Tactic.Monotonicity 314 0 -314 (-100.00%)
Mathlib.Tactic.NormNum 575 0 -575 (-100.00%)
Mathlib.Tactic.NormNum.Core 186 0 -186 (-100.00%)
Mathlib.Tactic.NormNum.OfScientific 564 0 -564 (-100.00%)
Mathlib.Tactic.NormNum.Pow 381 0 -381 (-100.00%)
Mathlib.Tactic.NormNum.Result 180 0 -180 (-100.00%)
Mathlib.Tactic.Positivity 504 0 -504 (-100.00%)
Mathlib.Tactic.Positivity.Basic 499 0 -499 (-100.00%)
Mathlib.Tactic.Positivity.Core 487 0 -487 (-100.00%)
Mathlib.Tactic.Propose 49 0 -49 (-100.00%)
Mathlib.Tactic.Ring 513 0 -513 (-100.00%)
Mathlib.Tactic.Ring.NamePolyVars 1 0 -1 (-100.00%)
Mathlib.Tactic.SplitIfs 48 0 -48 (-100.00%)
Mathlib.Tactic.Tauto 50 0 -50 (-100.00%)
Mathlib.Tactic.ToAdditive 66 0 -66 (-100.00%)
Mathlib.Tactic.ToDual 68 0 -68 (-100.00%)
Mathlib.Tactic.Widget.CommDiag 268 0 -268 (-100.00%)
Mathlib.Testing.Plausible.Functions 465 0 -465 (-100.00%)
Mathlib.Testing.Plausible.Sampleable 96 0 -96 (-100.00%)
Mathlib.Testing.Plausible.Testable 57 0 -57 (-100.00%)
Mathlib.Topology.Algebra.Group.GroupTopology 1035 0 -1035 (-100.00%)
Mathlib.Topology.Algebra.Module.StrongDual 1101 0 -1101 (-100.00%)
Mathlib.Topology.Category.CompHaus.Frm 1617 0 -1617 (-100.00%)
Mathlib.Topology.Compactness.Exterior 254 0 -254 (-100.00%)
Mathlib.Topology.Compactness.HilbertCubeEmbedding 1248 0 -1248 (-100.00%)
Mathlib.Topology.Compactness.PseudometrizableLindelof 254 0 -254 (-100.00%)
Mathlib.Topology.Covering 882 0 -882 (-100.00%)
Mathlib.Topology.Exterior 254 0 -254 (-100.00%)
Mathlib.Topology.FiberPartition 705 0 -705 (-100.00%)
Mathlib.Topology.Instances.ZMultiples 1214 0 -1214 (-100.00%)
Mathlib.Topology.LocallyFinite 604 0 -604 (-100.00%)
Mathlib.Topology.MetricSpace.Bounded 1028 0 -1028 (-100.00%)
Mathlib.Topology.MetricSpace.Cauchy 998 0 -998 (-100.00%)
Mathlib.Topology.MetricSpace.ProperSpace 1006 0 -1006 (-100.00%)
Mathlib.Topology.MetricSpace.Pseudo.Basic 986 0 -986 (-100.00%)
Mathlib.Topology.MetricSpace.Pseudo.Defs 889 0 -889 (-100.00%)
Mathlib.Topology.MetricSpace.Ultra.Basic 965 0 -965 (-100.00%)
Mathlib.Topology.OpenPartialHomeomorph 714 0 -714 (-100.00%)
Mathlib.Topology.PartialHomeomorph 254 0 -254 (-100.00%)
Mathlib.Topology.Piecewise 603 0 -603 (-100.00%)
Mathlib.Topology.Semicontinuous 1219 0 -1219 (-100.00%)
Mathlib.Topology.Sheaves.Alexandrov 1034 0 -1034 (-100.00%)
Mathlib.Util.AliasIn 2 0 -2 (-100.00%)
Mathlib.Util.DischargerAsTactic 49 0 -49 (-100.00%)
Mathlib.Util.Export 47 0 -47 (-100.00%)
Mathlib.Util.PPOptions 47 0 -47 (-100.00%)
Mathlib.Util.WhatsNew 47 0 -47 (-100.00%)
Import changes for all files
Files Import difference
There are 7603 files with changed transitive imports taking up over 327320 characters: this is too many to display!
You can run scripts/import_trans_difference.sh all locally to see the whole output.

Declarations diff

+ default_lean_files()
+ extract_docstrings(text:
+ file_has_h1_docstring(path:
+ has_h1_header(docstring:
+ main()
+ parse_args()

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for scripts/declarations_diff.sh contains some details about this script.

Increase in tech debt: (relative, absolute) = (18.00, 0.03)
Current number Change Type
717 18 total LoC in Deprecated files

Current commit 38592f505f
Reference commit 88bb6d226a

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@mathlib-merge-conflicts mathlib-merge-conflicts bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 20, 2026
@mathlib-merge-conflicts
Copy link

mathlib-merge-conflicts bot commented Feb 20, 2026

This pull request has conflicts, please merge master and resolve them.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) WIP Work in progress

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@harahu