chore: lake shake --add-public --keep-implied --keep-prefix --fix

[mathlib-nolints]

I am happy to shake some imports for you!

497 files changed · +584 imports added · -417 imports removed

---

workflow run for this PR
explain.txt

[github-actions]

PR summary 49ac088e17

Import changes exceeding 2%

%	File
+2.07%	Mathlib.Algebra.GroupWithZero.Units.Basic
+5.36%	Mathlib.CategoryTheory.Category.Cat.Limit
+2.30%	Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
+5.26%	Mathlib.CategoryTheory.Limits.Preserves.Yoneda
+5.82%	Mathlib.CategoryTheory.Limits.Types.Colimits
+5.61%	Mathlib.CategoryTheory.Limits.Types.Limits
+5.59%	Mathlib.CategoryTheory.Limits.Types.Yoneda
+5.25%	Mathlib.CategoryTheory.Limits.Yoneda
+2.50%	Mathlib.Order.Defs.LinearOrder
+16.95%	Mathlib.Tactic.CongrExclamation
+16.39%	Mathlib.Tactic.Convert
+2.74%	Mathlib.Tactic.FunProp.Elab
+3.33%	Mathlib.Tactic.FunProp.Types
+2.50%	Mathlib.Tactic.GRewrite.Elab
+60900.00%	Mathlib.Tactic.Linarith.NNRealPreprocessor
+33.33%	Mathlib.Tactic.Linter.Header
+25.00%	Mathlib.Tactic.Linter.Style
+100.00%	Mathlib.Tactic.Nontriviality.Core
+3.51%	Mathlib.Tactic.SetLike
+3.39%	Mathlib.Tactic.Simps.Basic
+3.39%	Mathlib.Tactic.Tauto

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Tactic.Linarith.NNRealPreprocessor	1	610	+609 (+60900.00%)
Mathlib.Tactic.Nontriviality.Core	2	4	+2 (+100.00%)
Mathlib.Computability.TMComputable	1024	256	-768 (-75.00%)
Mathlib.Data.Matrix.Action	791	256	-535 (-67.64%)
Mathlib.Data.Fintype.Units	751	256	-495 (-65.91%)
Mathlib.Data.Finite.Card	749	256	-493 (-65.82%)
Mathlib.Data.Rat.Cardinal	706	256	-450 (-63.74%)
Mathlib.Data.Matrix.DualNumber	1049	387	-662 (-63.11%)
Mathlib.Data.Matrix.Invertible	1012	388	-624 (-61.66%)
Mathlib.Data.Matrix.Bilinear	1008	387	-621 (-61.61%)
Mathlib.Computability.TMToPartrec	666	256	-410 (-61.56%)
Mathlib.Computability.TMConfig	644	256	-388 (-60.25%)
Mathlib.Order.Synonym	137	57	-80 (-58.39%)
Mathlib.AlgebraicGeometry.RationalMap	2459	1112	-1347 (-54.78%)
Mathlib.Data.FunLike.Ring	278	137	-141 (-50.72%)
Mathlib.Tactic.Linter.DocString	2	1	-1 (-50.00%)
Mathlib.Computability.PostTuringMachine	483	254	-229 (-47.41%)
Mathlib.InformationTheory.Coding.UniquelyDecodable	181	102	-79 (-43.65%)
Mathlib.Data.Matrix.Cartan	1218	689	-529 (-43.43%)
Mathlib.AlgebraicTopology.SimplicialComplex.Basic	1087	627	-460 (-42.32%)
Mathlib.RingTheory.Regular.Depth	1837	1105	-732 (-39.85%)
Mathlib.Logic.IsEmpty	90	56	-34 (-37.78%)
Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty	643	412	-231 (-35.93%)
Mathlib.Geometry.Manifold.VectorBundle.SmoothSection	2190	1413	-777 (-35.48%)
Mathlib.Tactic.Linter.Header	3	4	+1 (+33.33%)
Mathlib.Tactic.Algebra.Lemmas	768	517	-251 (-32.68%)
Mathlib.Condensed.Light.CartesianClosed	1908	1290	-618 (-32.39%)
Mathlib.Condensed.CartesianClosed	1840	1290	-550 (-29.89%)
Mathlib.Computability.Tape	342	251	-91 (-26.61%)
Mathlib.Analysis.ODE.DiscreteGronwall	1934	1425	-509 (-26.32%)
Mathlib.Lean.Elab.InfoTree	8	6	-2 (-25.00%)
Mathlib.Tactic.Linter.Style	4	5	+1 (+25.00%)
Mathlib.NumberTheory.NumberField.FinitePlaces	3026	2275	-751 (-24.82%)
Mathlib.Computability.StateTransition	468	369	-99 (-21.15%)
Mathlib.Geometry.Convex.ConvexSpace.Module	1038	862	-176 (-16.96%)
Mathlib.Tactic.CongrExclamation	59	69	+10 (+16.95%)
Mathlib.Topology.Spectral.ConstructibleTopology	896	747	-149 (-16.63%)
Mathlib.Tactic.Convert	61	71	+10 (+16.39%)
Mathlib.Analysis.Normed.Module.Complemented	2049	1745	-304 (-14.84%)
Mathlib.Order.Lex	137	118	-19 (-13.87%)
Mathlib.Data.Nat.Cast.Synonym	151	132	-19 (-12.58%)
Mathlib.Topology.Homeomorph.Quotient	714	625	-89 (-12.46%)
Mathlib.Analysis.ConstantSpeed	1612	1414	-198 (-12.28%)
Mathlib.Algebra.Module.Injective	1127	1004	-123 (-10.91%)
Mathlib.Order.SaddlePoint	421	380	-41 (-9.74%)
Mathlib.Data.Bool.Count	417	377	-40 (-9.59%)
Mathlib.NumberTheory.ModularForms.CuspFormSubmodule	3172	2868	-304 (-9.58%)
Mathlib.Analysis.Normed.Group.Tannery	1612	1463	-149 (-9.24%)
Mathlib.RepresentationTheory.Continuous.Basic	1791	1634	-157 (-8.77%)
Mathlib.MeasureTheory.Measure.CharacteristicFunction	2578	2360	-218 (-8.46%)
Mathlib.Order.ConditionallyCompletePartialOrder.Basic	264	242	-22 (-8.33%)
Mathlib.LinearAlgebra.LinearIndependent.BaseChange	1268	1163	-105 (-8.28%)
Mathlib.RingTheory.IntegralClosure.IntegralRestrict	2021	1859	-162 (-8.02%)
Mathlib.Analysis.Normed.Module.Bases	2047	1890	-157 (-7.67%)
Mathlib.Order.OmegaCompletePartialOrder	405	374	-31 (-7.65%)
Mathlib.Order.CompletePartialOrder	407	378	-29 (-7.13%)
Mathlib.Order.GaloisConnection.Defs	173	161	-12 (-6.94%)
Mathlib.Algebra.MvPolynomial.Cardinal	1220	1141	-79 (-6.48%)
Mathlib.LinearAlgebra.FixedSubmodule	1136	1065	-71 (-6.25%)
Mathlib.Order.BourbakiWitt	417	391	-26 (-6.24%)
Mathlib.Data.Int.Order.Basic	97	91	-6 (-6.19%)
Mathlib.Algebra.Group.Submonoid.Saturation	428	402	-26 (-6.07%)
Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset	616	579	-37 (-6.01%)
Mathlib.Testing.Plausible.Sampleable	102	96	-6 (-5.88%)
Mathlib.CategoryTheory.Limits.Types.Colimits	447	473	+26 (+5.82%)
Mathlib.CategoryTheory.Limits.Types.Limits	446	471	+25 (+5.61%)
Mathlib.CategoryTheory.Limits.Types.Yoneda	447	472	+25 (+5.59%)
Mathlib.CategoryTheory.Category.Cat.Limit	448	472	+24 (+5.36%)
Mathlib.CategoryTheory.Limits.Preserves.Yoneda	456	480	+24 (+5.26%)
Mathlib.CategoryTheory.Limits.Yoneda	457	481	+24 (+5.25%)
Mathlib.CategoryTheory.Bicategory.Span.Basic	687	652	-35 (-5.09%)
Mathlib.LinearAlgebra.QuadraticForm.Real	1906	1812	-94 (-4.93%)
Mathlib.Algebra.Category.MonCat.Colimits	487	463	-24 (-4.93%)
Mathlib.Data.List.Forall2	267	254	-13 (-4.87%)
Mathlib.RingTheory.DedekindDomain.Factorization	2149	2052	-97 (-4.51%)
Mathlib.Data.List.Perm.Basic	271	259	-12 (-4.43%)
Mathlib.Data.List.DropRight	280	268	-12 (-4.29%)
Mathlib.Data.Real.Archimedean	694	665	-29 (-4.18%)
Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset	1010	968	-42 (-4.16%)
Mathlib.Algebra.Homology.ModelCategory.Lifting	1294	1241	-53 (-4.10%)
Mathlib.Analysis.Convex.MetricSpace	1495	1442	-53 (-3.55%)
Mathlib.Tactic.SetLike	57	59	+2 (+3.51%)
Mathlib.Analysis.Calculus.FDeriv.Affine	1748	1687	-61 (-3.49%)
Mathlib.Algebra.Group.Submonoid.Support	663	640	-23 (-3.47%)
Mathlib.RingTheory.FormalGroup.Basic	1493	1442	-51 (-3.42%)
Mathlib.Tactic.Simps.Basic	59	61	+2 (+3.39%)
Mathlib.Tactic.Tauto	59	61	+2 (+3.39%)
Mathlib.Tactic.FunProp.Types	60	62	+2 (+3.33%)
Mathlib.CategoryTheory.Sites.Over	1086	1050	-36 (-3.31%)
Mathlib.Probability.Decision.Risk.Countable	1692	1636	-56 (-3.31%)
Mathlib.LinearAlgebra.SModEq.Pow	1180	1141	-39 (-3.31%)
Mathlib.Data.Nat.Cast.WithTop	224	217	-7 (-3.12%)
Mathlib.Computability.TuringMachine.Config	643	623	-20 (-3.11%)
Mathlib.Topology.Instances.ENNReal.ENatENNReal	1325	1284	-41 (-3.09%)
Mathlib.RingTheory.MvPowerSeries.Equiv	1789	1737	-52 (-2.91%)
Mathlib.Algebra.Regular.Defs	69	67	-2 (-2.90%)
Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv	1762	1712	-50 (-2.84%)
Mathlib.CategoryTheory.Monoidal.Cartesian.Normal	802	780	-22 (-2.74%)
Mathlib.LinearAlgebra.TensorProduct.Defs	839	816	-23 (-2.74%)
Mathlib.Tactic.FunProp.Elab	73	75	+2 (+2.74%)
Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule	2509	2441	-68 (-2.71%)
Mathlib.CategoryTheory.Triangulated.TStructure.Heart	1130	1100	-30 (-2.65%)
Mathlib.Algebra.Order.Field.Pointwise	314	306	-8 (-2.55%)
Mathlib.Algebra.LinearRecurrence	1346	1312	-34 (-2.53%)
Mathlib.Geometry.Convex.Set	876	854	-22 (-2.51%)
Mathlib.Order.Defs.LinearOrder	80	82	+2 (+2.50%)
Mathlib.Tactic.GRewrite.Elab	80	82	+2 (+2.50%)
Mathlib.Data.List.Sigma	285	278	-7 (-2.46%)
Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct	608	622	+14 (+2.30%)
Mathlib.GroupTheory.GroupAction.MultipleTransitivity	1176	1149	-27 (-2.30%)
Mathlib.Analysis.InnerProductSpace.Positive	2485	2430	-55 (-2.21%)
Mathlib.GroupTheory.GroupAction.MultiplePrimitivity	1177	1151	-26 (-2.21%)
Mathlib.GroupTheory.Perm.MaximalSubgroups	1179	1153	-26 (-2.21%)
Mathlib.Algebra.GroupWithZero.Units.Basic	145	148	+3 (+2.07%)
Mathlib.MeasureTheory.Measure.RegularityCompacts	1561	1531	-30 (-1.92%)
Mathlib.Algebra.Order.SuccPred	423	415	-8 (-1.89%)
Mathlib.Data.Set.Dissipate	584	573	-11 (-1.88%)
Mathlib.Tactic.ApplyWith	56	57	+1 (+1.79%)
Mathlib.Tactic.DSimpPercent	56	57	+1 (+1.79%)
Mathlib.Data.Finset.Attr	57	58	+1 (+1.75%)
Mathlib.Data.Int.DivMod	57	56	-1 (-1.75%)
Mathlib.Tactic.Linter.FindDeprecations	57	56	-1 (-1.75%)
Mathlib.Data.Int.Basic	118	116	-2 (-1.69%)
Mathlib.Tactic.Attr.Core	59	60	+1 (+1.69%)
Mathlib.Tactic.Linter.TextBased	59	58	-1 (-1.69%)
Mathlib.Algebra.Group.Even	183	180	-3 (-1.64%)
Mathlib.Tactic.Hint	62	61	-1 (-1.61%)
Mathlib.Algebra.MvPolynomial.Division	1086	1069	-17 (-1.57%)
Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit	645	655	+10 (+1.55%)
Mathlib.Tactic.Widget.Calc	65	64	-1 (-1.54%)
Mathlib.Tactic.Widget.InteractiveUnfold	65	64	-1 (-1.54%)
Mathlib.AlgebraicGeometry.Noetherian	2455	2418	-37 (-1.51%)
Mathlib.Tactic.Widget.Conv	67	66	-1 (-1.49%)
Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic	619	628	+9 (+1.45%)
Mathlib.Tactic.Push	69	70	+1 (+1.45%)
Mathlib.Order.Defs.PartialOrder	71	70	-1 (-1.41%)
Mathlib.Order.Notation	72	71	-1 (-1.39%)
Mathlib.RingTheory.AlgebraicIndependent.Defs	1083	1068	-15 (-1.39%)
Mathlib.GroupTheory.FreeGroup.Basic	441	435	-6 (-1.36%)
Mathlib.SetTheory.Cardinal.Embedding	765	755	-10 (-1.31%)
Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly	618	626	+8 (+1.29%)
Mathlib.Tactic.GRewrite.Core	79	80	+1 (+1.27%)
Mathlib.Data.Ordmap.Ordnode	161	159	-2 (-1.24%)
Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution	1291	1275	-16 (-1.24%)
Mathlib.Condensed.Light.Monoidal	2039	2015	-24 (-1.18%)
Mathlib.Analysis.SpecificLimits.RCLike	1626	1607	-19 (-1.17%)
Mathlib.NumberTheory.Padics.WithVal	2238	2212	-26 (-1.16%)
Mathlib.LinearAlgebra.Transvection.Basic	1732	1712	-20 (-1.15%)
Mathlib.FieldTheory.Fixed	1677	1658	-19 (-1.13%)
Mathlib.LinearAlgebra.Matrix.Integer	811	802	-9 (-1.11%)
Mathlib.Tactic.Peel	273	276	+3 (+1.10%)
Mathlib.Data.Prod.Basic	94	93	-1 (-1.06%)
Mathlib.Tactic.Sat.FromLRAT	94	95	+1 (+1.06%)
Mathlib.Data.Part	192	190	-2 (-1.04%)
Mathlib.CategoryTheory.Monoidal.Internal.Limits	481	476	-5 (-1.04%)
Mathlib.Data.Option.Basic	97	96	-1 (-1.03%)
Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered	1172	1160	-12 (-1.02%)
Mathlib.Algebra.Module.SpanRank	1318	1305	-13 (-0.99%)
Mathlib.Logic.Nontrivial.Basic	106	105	-1 (-0.94%)
Mathlib.Algebra.Order.Monoid.Canonical.Defs	213	211	-2 (-0.94%)
Mathlib.LinearAlgebra.Matrix.MvPolynomial	1288	1276	-12 (-0.93%)
Mathlib.RingTheory.TensorProduct.IsBaseChangeRightExact	1192	1181	-11 (-0.92%)
Mathlib.Tactic.Widget.StringDiagram	328	331	+3 (+0.91%)
Mathlib.Data.Real.StarOrdered	1322	1310	-12 (-0.91%)
Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex	891	899	+8 (+0.90%)
Mathlib.AlgebraicTopology.SimplicialSet.Boundary	917	925	+8 (+0.87%)
Mathlib.Data.Nat.BitIndices	459	455	-4 (-0.87%)
Mathlib.Data.Finsupp.PWO	598	593	-5 (-0.84%)
Mathlib.CategoryTheory.Abelian.Preradical.Colon	840	833	-7 (-0.83%)
Mathlib.LinearAlgebra.TensorProduct.Basic	840	833	-7 (-0.83%)
Mathlib.AlgebraicTopology.SimplicialSet.Monoidal	983	975	-8 (-0.81%)
Mathlib.Algebra.Group.Units.Basic	123	124	+1 (+0.81%)
Mathlib.RingTheory.LocalProperties.InjectiveDimension	2129	2112	-17 (-0.80%)
Mathlib.GroupTheory.SpecificGroups.Alternating	1140	1131	-9 (-0.79%)
Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices	890	897	+7 (+0.79%)
Mathlib.RingTheory.FreeCommRing	1195	1186	-9 (-0.75%)
Mathlib.Algebra.Divisibility.Units	270	272	+2 (+0.74%)
Mathlib.RingTheory.Polynomial.SmallDegreeVieta	1356	1346	-10 (-0.74%)
Mathlib.Topology.Defs.Basic	136	137	+1 (+0.74%)
Mathlib.Data.List.Zip	276	278	+2 (+0.72%)
Mathlib.Control.Traversable.Equiv	139	140	+1 (+0.72%)
Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM	1538	1527	-11 (-0.72%)
Mathlib.Tactic.Zify	141	140	-1 (-0.71%)
Mathlib.Tactic.ModCases	425	428	+3 (+0.71%)
Mathlib.FieldTheory.IntermediateField.Adjoin.Basic	1703	1691	-12 (-0.70%)
Mathlib.RingTheory.MvPowerSeries.Evaluation	1443	1433	-10 (-0.69%)
Mathlib.Tactic.NormNum.NatLog	590	594	+4 (+0.68%)
Mathlib.Logic.Embedding.Basic	149	148	-1 (-0.67%)
Mathlib.Data.Int.GCD	302	304	+2 (+0.66%)
Mathlib.NumberTheory.RatFunc.Ostrowski	2301	2286	-15 (-0.65%)
Mathlib.MeasureTheory.Integral.Asymptotics	2315	2300	-15 (-0.65%)
Mathlib.Algebra.MvPolynomial.Funext	1252	1244	-8 (-0.64%)
Mathlib.RingTheory.MvPolynomial.Symmetric.Defs	1105	1098	-7 (-0.63%)
Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities	1106	1099	-7 (-0.63%)
Mathlib.Algebra.Order.Group.Indicator	318	316	-2 (-0.63%)
Mathlib.Tactic.Simproc.FinsetInterval	642	646	+4 (+0.62%)
Mathlib.CategoryTheory.Monoidal.Widesubcategory	494	491	-3 (-0.61%)
Mathlib.Combinatorics.Compactness	664	668	+4 (+0.60%)
Mathlib.Order.Monotone.Basic	167	166	-1 (-0.60%)
Mathlib.Data.QPF.Multivariate.Constructions.Cofix	527	530	+3 (+0.57%)
Mathlib.Dynamics.FixedPoints.Topology	704	700	-4 (-0.57%)
Mathlib.Order.Disjoint	177	176	-1 (-0.56%)
Mathlib.Topology.Maps.Strict.Basic	715	719	+4 (+0.56%)
Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss	2510	2496	-14 (-0.56%)
Mathlib.Analysis.SpecialFunctions.Stirling	2513	2499	-14 (-0.56%)
Mathlib.RingTheory.MvPolynomial.Homogeneous	1295	1288	-7 (-0.54%)
Mathlib.Data.Set.Insert	186	185	-1 (-0.54%)
Mathlib.Tactic.FinCases	373	375	+2 (+0.54%)
Mathlib.Data.Fintype.Order	569	572	+3 (+0.53%)
Mathlib.RingTheory.MvPolynomial.Localization	1332	1325	-7 (-0.53%)
Mathlib.Tactic.NormNum.Result	193	194	+1 (+0.52%)
Mathlib.Order.PartialSups	581	584	+3 (+0.52%)
Mathlib.Algebra.NonAssoc.PreLie.Basic	395	393	-2 (-0.51%)
Mathlib.Algebra.Order.Hom.Lattice	595	598	+3 (+0.50%)
Mathlib.Algebra.Ring.CharZero	397	399	+2 (+0.50%)
Mathlib.NumberTheory.ModularForms.Basic	2780	2766	-14 (-0.50%)
Mathlib.RingTheory.PowerSeries.GaussNorm	1404	1397	-7 (-0.50%)
Mathlib.Order.Disjointed	605	608	+3 (+0.50%)
Mathlib.GroupTheory.GroupAction.Defs	405	407	+2 (+0.49%)
Mathlib.CategoryTheory.Sites.CoverPreserving	818	822	+4 (+0.49%)
Mathlib.Analysis.LocallyConvex.Polar	1435	1428	-7 (-0.49%)
Mathlib.Order.Atoms	411	413	+2 (+0.49%)
Mathlib.Algebra.Category.MonCat.FilteredColimits	617	620	+3 (+0.49%)
Mathlib.Algebra.Order.Nonneg.Basic	417	419	+2 (+0.48%)
Mathlib.Analysis.ODE.ExistUnique	2516	2504	-12 (-0.48%)
Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional	1476	1469	-7 (-0.47%)
Mathlib.Algebra.Lie.CartanCriterion	1898	1889	-9 (-0.47%)
Mathlib.Order.Bounded	211	210	-1 (-0.47%)
Mathlib.Analysis.Complex.Harmonic.Poisson	2546	2534	-12 (-0.47%)
Mathlib.Data.Fintype.Basic	426	428	+2 (+0.47%)
Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique	2557	2545	-12 (-0.47%)
Mathlib.NumberTheory.RamificationInertia.Unramified	2347	2336	-11 (-0.47%)
Mathlib.Topology.Sheaves.LocalPredicate	1068	1073	+5 (+0.47%)
Mathlib.Algebra.BigOperators.Intervals	648	651	+3 (+0.46%)
Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus	2388	2377	-11 (-0.46%)
Mathlib.CategoryTheory.MorphismProperty.CommaSites	1098	1103	+5 (+0.46%)
Mathlib.CategoryTheory.Sites.Descent.Precoverage	1098	1103	+5 (+0.46%)
Mathlib.RingTheory.Smooth.Quotient	2207	2197	-10 (-0.45%)
Mathlib.RingTheory.Polynomial.Basic	1334	1328	-6 (-0.45%)
Mathlib.Data.Nat.WithBot	228	227	-1 (-0.44%)
Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric	2530	2519	-11 (-0.43%)
Mathlib.Algebra.Category.Ring.Topology	1617	1610	-7 (-0.43%)
Mathlib.Geometry.Manifold.Complex	2547	2536	-11 (-0.43%)
Mathlib.NumberTheory.Chebyshev	2551	2540	-11 (-0.43%)
Mathlib.RingTheory.RingHom.FinitePresentation	1858	1850	-8 (-0.43%)
Mathlib.RingTheory.MvPolynomial	1405	1399	-6 (-0.43%)
Mathlib.Analysis.Complex.JensenFormula	2610	2599	-11 (-0.42%)
Mathlib.RingTheory.DedekindDomain.Different	2380	2370	-10 (-0.42%)
Mathlib.RingTheory.RingHom.FiniteType	1680	1673	-7 (-0.42%)
Mathlib.Tactic.Ring.Common	482	484	+2 (+0.41%)
Mathlib.Tactic.Ring.Basic	483	485	+2 (+0.41%)
Mathlib.CategoryTheory.Sites.Hypercover.One	731	734	+3 (+0.41%)
Mathlib.Topology.Compactness.CountablyCompact	733	736	+3 (+0.41%)
Mathlib.Algebra.Group.Pi.Lemmas	245	244	-1 (-0.41%)
Mathlib.Analysis.Complex.UpperHalfPlane.Manifold	2710	2699	-11 (-0.41%)
Mathlib.Tactic.Simproc.Factors	496	498	+2 (+0.40%)
Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable	2737	2726	-11 (-0.40%)
Mathlib.LinearAlgebra.Projectivization.Action	1746	1739	-7 (-0.40%)
Mathlib.Data.List.InsertIdx	251	252	+1 (+0.40%)
Mathlib.Data.List.Palindrome	252	253	+1 (+0.40%)
Mathlib.Algebra.Tropical.Basic	253	252	-1 (-0.40%)
Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan	1524	1518	-6 (-0.39%)
Mathlib.AlgebraicGeometry.Sites.AffineEtale	2798	2787	-11 (-0.39%)
Mathlib.Algebra.SkewPolynomial.Basic	1019	1015	-4 (-0.39%)
Mathlib.MeasureTheory.Measure.Stieltjes	1530	1524	-6 (-0.39%)
Mathlib.Data.List.ProdSigma	256	257	+1 (+0.39%)
Mathlib.Tactic.Algebra.Basic	769	772	+3 (+0.39%)
Mathlib.NumberTheory.Height.MvPolynomial	1811	1804	-7 (-0.39%)
Mathlib.Data.List.Basic	265	266	+1 (+0.38%)
Mathlib.Data.List.Nodup	268	269	+1 (+0.37%)
Mathlib.Combinatorics.Enumerative.Catalan.Tree	816	819	+3 (+0.37%)
Mathlib.CategoryTheory.Functor.Basic	273	274	+1 (+0.37%)
Mathlib.Data.Nat.Digits.Lemmas	827	830	+3 (+0.36%)
Mathlib.Data.Nat.Choose.Lucas	1386	1381	-5 (-0.36%)
Mathlib.Combinatorics.Quiver.Covering	279	280	+1 (+0.36%)
Mathlib.Analysis.Complex.Schwarz	2531	2522	-9 (-0.36%)
Mathlib.Analysis.Complex.Harmonic.Liouville	2540	2531	-9 (-0.35%)
Mathlib.Algebra.Homology.HomologicalComplexAbelian	852	849	-3 (-0.35%)
Mathlib.GroupTheory.IndexNSmul	1430	1425	-5 (-0.35%)
Mathlib.Order.Filter.AtTopBot.CompleteLattice	292	293	+1 (+0.34%)
Mathlib.RingTheory.Valuation.ValuativeRel.Basic	1173	1169	-4 (-0.34%)
Mathlib.Algebra.BigOperators.Group.List.Basic	302	303	+1 (+0.33%)
Mathlib.Analysis.Calculus.IteratedDeriv.Analytic	1819	1813	-6 (-0.33%)
Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent	1226	1230	+4 (+0.33%)
Mathlib.RepresentationTheory.Homological.Resolution	1854	1848	-6 (-0.32%)
Mathlib.Computability.Reduce	620	622	+2 (+0.32%)
Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PushoutProduct	1248	1252	+4 (+0.32%)
Mathlib.Topology.Algebra.UniformRing	1251	1247	-4 (-0.32%)
Mathlib.Geometry.Manifold.WhitneyEmbedding	2541	2533	-8 (-0.31%)
Mathlib.Algebra.GroupWithZero.WithZero	318	319	+1 (+0.31%)
Mathlib.Probability.Moments.IntegrableExpMul	2265	2258	-7 (-0.31%)
Mathlib.Algebra.Group.Int.Even	324	323	-1 (-0.31%)
Mathlib.Algebra.Group.Subgroup.Defs	325	326	+1 (+0.31%)
Mathlib.Data.Real.CompleteField	1313	1309	-4 (-0.30%)
Mathlib.Data.Real.Hom	1313	1309	-4 (-0.30%)
Mathlib.Topology.DiscreteSubset	690	692	+2 (+0.29%)
Mathlib.RingTheory.OreLocalization.Basic	348	349	+1 (+0.29%)
Mathlib.Algebra.Group.End	349	350	+1 (+0.29%)
Mathlib.Analysis.Normed.Module.Dual	2098	2092	-6 (-0.29%)
Mathlib.FieldTheory.IsAlgClosed.Basic	1756	1751	-5 (-0.28%)
Mathlib.NumberTheory.Bernoulli	2112	2106	-6 (-0.28%)
Mathlib.Algebra.Module.Submodule.Invariant	709	711	+2 (+0.28%)
Mathlib.Topology.CWComplex.Classical.Graph	1424	1420	-4 (-0.28%)
Mathlib.Topology.Instances.Int	1068	1071	+3 (+0.28%)
Mathlib.RingTheory.Coalgebra.TensorProduct	1070	1073	+3 (+0.28%)
Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic	2205	2199	-6 (-0.27%)
Mathlib.Data.List.FinRange	370	369	-1 (-0.27%)
Mathlib.Data.List.Sort	372	371	-1 (-0.27%)
Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology	1861	1856	-5 (-0.27%)
Mathlib.CategoryTheory.Sites.Hypercover.Saturate	753	755	+2 (+0.27%)
Mathlib.Algebra.BigOperators.Finprod	760	762	+2 (+0.26%)
Mathlib.Tactic.NormNum.Pow	388	389	+1 (+0.26%)
Mathlib.Combinatorics.SimpleGraph.Hamiltonian	779	781	+2 (+0.26%)
Mathlib.CategoryTheory.ObjectProperty.Opposite	392	391	-1 (-0.26%)
Mathlib.ModelTheory.FinitelyGenerated	788	790	+2 (+0.25%)
Mathlib.CategoryTheory.Sites.Continuous	801	803	+2 (+0.25%)
Mathlib.Analysis.Convex.FunctionTopology	1203	1206	+3 (+0.25%)
Mathlib.RingTheory.DedekindDomain.Instances	2064	2059	-5 (-0.24%)
Mathlib.Analysis.Calculus.Implicit	2081	2076	-5 (-0.24%)
Mathlib.Algebra.Group.Subgroup.Ker	418	419	+1 (+0.24%)
Mathlib.NumberTheory.FactorisationProperties	836	838	+2 (+0.24%)
Mathlib.Order.FixedPoints	419	420	+1 (+0.24%)
Mathlib.Tactic.NormNum.Prime	420	421	+1 (+0.24%)
Mathlib.FieldTheory.Galois.NormalBasis	2102	2097	-5 (-0.24%)
Mathlib.Analysis.Normed.Module.DoubleDual	2112	2107	-5 (-0.24%)
Mathlib.Tactic.Algebraize	854	856	+2 (+0.23%)
Mathlib.Geometry.Manifold.ContMDiff.Atlas	2173	2168	-5 (-0.23%)
Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions	2175	2170	-5 (-0.23%)
Mathlib.Geometry.Manifold.Algebra.Monoid	2178	2173	-5 (-0.23%)
Mathlib.Geometry.Manifold.Algebra.LieGroup	2179	2174	-5 (-0.23%)
Mathlib.Data.Set.Card.Arithmetic	876	878	+2 (+0.23%)
Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential	2190	2185	-5 (-0.23%)
Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable	2192	2187	-5 (-0.23%)
Mathlib.NumberTheory.Height.Basic	1754	1758	+4 (+0.23%)
Mathlib.Geometry.Manifold.VectorBundle.Tensoriality	2201	2196	-5 (-0.23%)
Mathlib.Geometry.Manifold.VectorField.LieBracket	2220	2215	-5 (-0.23%)
Mathlib.Data.Nat.Count	446	447	+1 (+0.22%)
Mathlib.CategoryTheory.Limits.Constructions.WidePullbackOfTerminal	451	450	-1 (-0.22%)
Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Terminal	453	452	-1 (-0.22%)
Mathlib.Analysis.Calculus.AbsolutelyMonotone	1817	1813	-4 (-0.22%)
Mathlib.MeasureTheory.Integral.Bochner.Basic	2273	2268	-5 (-0.22%)
Mathlib.Geometry.Manifold.Instances.Icc	2279	2274	-5 (-0.22%)
Mathlib.CategoryTheory.Limits.Preserves.SigmaConst	473	474	+1 (+0.21%)
Mathlib.CategoryTheory.Shift.Adjunction	488	487	-1 (-0.20%)
Mathlib.AlgebraicTopology.SimplicialCategory.Basic	985	987	+2 (+0.20%)
Mathlib.NumberTheory.NumberField.Completion.Ramification	3006	3000	-6 (-0.20%)
Mathlib.NumberTheory.NumberField.Completion.FinitePlace	3025	3019	-6 (-0.20%)
Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral	2536	2541	+5 (+0.20%)
Mathlib.LinearAlgebra.Vandermonde	1523	1526	+3 (+0.20%)
Mathlib.Analysis.Asymptotics.TVS	1526	1523	-3 (-0.20%)
Mathlib.Tactic.Positivity.Basic	509	508	-1 (-0.20%)
Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap	1540	1543	+3 (+0.19%)
Mathlib.Data.Nat.Totient	1033	1035	+2 (+0.19%)
Mathlib.Analysis.Convex.Approximation	2074	2070	-4 (-0.19%)
Mathlib.Analysis.Normed.Module.FiniteDimension	2081	2077	-4 (-0.19%)
Mathlib.GroupTheory.DivisibleHull	1045	1047	+2 (+0.19%)
Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs	1058	1060	+2 (+0.19%)
Mathlib.Algebra.Polynomial.Eval.Coeff	1059	1061	+2 (+0.19%)
Mathlib.Analysis.Convex.Segment	1059	1061	+2 (+0.19%)
Mathlib.Analysis.PSeries	2122	2118	-4 (-0.19%)
Mathlib.RingTheory.Coalgebra.CoassocSimps	1066	1068	+2 (+0.19%)
Mathlib.NumberTheory.LSeries.Injectivity	2134	2130	-4 (-0.19%)
Mathlib.RingTheory.Localization.AtPrime.Extension	2148	2144	-4 (-0.19%)
Mathlib.Analysis.InnerProductSpace.PiL2	2162	2158	-4 (-0.19%)
Mathlib.Data.Finsupp.Pointwise	541	540	-1 (-0.18%)
Mathlib.Topology.Algebra.Ring.Basic	1089	1091	+2 (+0.18%)
Mathlib.Analysis.Distribution.SchwartzSpace.Basic	2799	2794	-5 (-0.18%)
Mathlib.Analysis.Calculus.FDeriv.OfCompLeft	1681	1684	+3 (+0.18%)
Mathlib.NumberTheory.Primorial	1133	1135	+2 (+0.18%)
Mathlib.MeasureTheory.Group.Integral	2274	2270	-4 (-0.18%)
Mathlib.MeasureTheory.Measure.HasOuterApproxClosed	2283	2279	-4 (-0.18%)
Mathlib.MeasureTheory.Integral.Bochner.SumMeasure	2287	2283	-4 (-0.17%)
Mathlib.Algebra.Order.Ring.Archimedean	1156	1158	+2 (+0.17%)
Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation	2900	2895	-5 (-0.17%)
Mathlib.Probability.Distributions.Gaussian.CharFun	2902	2897	-5 (-0.17%)
Mathlib.Probability.Distributions.Gaussian.Multivariate	2906	2901	-5 (-0.17%)
Mathlib.Algebra.Module.ZLattice.Summable	2353	2349	-4 (-0.17%)
Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant	2363	2359	-4 (-0.17%)
Mathlib.Topology.Sheaves.Points	1186	1188	+2 (+0.17%)
Mathlib.AlgebraicGeometry.Morphisms.Finite	2375	2379	+4 (+0.17%)
Mathlib.Algebra.Category.AlgCat.FilteredColimits	1193	1195	+2 (+0.17%)
Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc	1206	1208	+2 (+0.17%)
Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic	1225	1223	-2 (-0.16%)
Mathlib.Data.ZMod.Coprime	1239	1241	+2 (+0.16%)
Mathlib.Topology.Algebra.Valued.ValuativeRel	1862	1859	-3 (-0.16%)
Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity	1895	1898	+3 (+0.16%)
Mathlib.Data.Rat.NatSqrt.Real	1315	1313	-2 (-0.15%)
Mathlib.Computability.TuringMachine.ToPartrec	665	666	+1 (+0.15%)
Mathlib.RingTheory.MvPowerSeries.GaussNorm	1348	1346	-2 (-0.15%)
Mathlib.Combinatorics.Additive.AP.Three.Defs	675	676	+1 (+0.15%)
Mathlib.Algebra.MonoidAlgebra.Defs	689	690	+1 (+0.15%)
Mathlib.LinearAlgebra.Projectivization.Collinear	1384	1382	-2 (-0.14%)
Mathlib.NumberTheory.LSeries.PrimesInAP	3474	3469	-5 (-0.14%)
Mathlib.Combinatorics.Derangements.Basic	705	706	+1 (+0.14%)
Mathlib.Algebra.Homology.ModelCategory.Injective	1416	1418	+2 (+0.14%)
Mathlib.Analysis.Asymptotics.Lemmas	1474	1472	-2 (-0.14%)
Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind	2217	2220	+3 (+0.14%)
Mathlib.Algebra.Module.Submodule.Pointwise	757	758	+1 (+0.13%)
Mathlib.SetTheory.Cardinal.Pigeonhole	759	758	-1 (-0.13%)
Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed	2347	2350	+3 (+0.13%)
Mathlib.GroupTheory.Congruence.BigOperators	785	784	-1 (-0.13%)
Mathlib.InformationTheory.Coding.KraftMcMillan	1582	1580	-2 (-0.13%)
Mathlib.RingTheory.Extension.Presentation.Basic	1604	1606	+2 (+0.12%)
Mathlib.LinearAlgebra.TensorProduct.Map	841	842	+1 (+0.12%)
Mathlib.RingTheory.Polynomial.IsIntegral	1682	1684	+2 (+0.12%)
Mathlib.NumberTheory.FLT.Polynomial	1691	1693	+2 (+0.12%)
Mathlib.FieldTheory.ChevalleyWarning	1727	1729	+2 (+0.12%)
Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale	2701	2704	+3 (+0.11%)
Mathlib.Topology.LocallyFinsupp	901	902	+1 (+0.11%)
Mathlib.Algebra.Algebra.Unitization	918	917	-1 (-0.11%)
Mathlib.Analysis.Calculus.DerivativeTest	1878	1880	+2 (+0.11%)
Mathlib.Analysis.Calculus.LogDeriv	1884	1882	-2 (-0.11%)
Mathlib.Topology.LocallyFinsupp.Pushforward	947	948	+1 (+0.11%)
Mathlib.RingTheory.Finiteness.Descent	2002	2000	-2 (-0.10%)
Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions	1002	1003	+1 (+0.10%)
Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem	1125	1126	+1 (+0.09%)
Mathlib.Analysis.Complex.RiemannMapping	2303	2305	+2 (+0.09%)
Mathlib.Algebra.Category.AlgCat.Basic	1170	1171	+1 (+0.09%)
Mathlib.Algebra.MvPolynomial.Equiv	1174	1175	+1 (+0.09%)
Mathlib.AlgebraicGeometry.Morphisms.FlatRank	2534	2536	+2 (+0.08%)
Mathlib.RingTheory.MvPolynomial.MonomialOrder	1303	1304	+1 (+0.08%)
Mathlib.Probability.Distributions.TwoValued	2702	2704	+2 (+0.07%)
Mathlib.Probability.Distributions.Binomial	2765	2767	+2 (+0.07%)
Mathlib.Algebra.MvPolynomial.Nilpotent	1386	1387	+1 (+0.07%)
Mathlib.RingTheory.MvPolynomial.Ideal	1395	1396	+1 (+0.07%)
Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion	2844	2842	-2 (-0.07%)
Mathlib.Algebra.Homology.DerivedCategory.Ext.Map	1424	1425	+1 (+0.07%)
Mathlib.Probability.Distributions.Poisson.PoissonLimitThm	2873	2871	-2 (-0.07%)
Mathlib.RingTheory.KrullDimension.NonZeroDivisors	1522	1523	+1 (+0.07%)
Mathlib.Dynamics.BirkhoffSum.NormedSpace	1604	1605	+1 (+0.06%)
Mathlib.Probability.UniformOn	1657	1656	-1 (-0.06%)
Mathlib.Algebra.Category.ModuleCat.Ext.Basic	1684	1683	-1 (-0.06%)
Mathlib.FieldTheory.Finite.Polynomial	1745	1746	+1 (+0.06%)
Mathlib.FieldTheory.CardinalEmb	1808	1809	+1 (+0.06%)
Mathlib.FieldTheory.PurelyInseparable.AdjoinPthRoots	1808	1807	-1 (-0.06%)
Mathlib.Analysis.Complex.CanonicalDecomposition	2002	2003	+1 (+0.05%)

Import changes for all files

Files	Import difference
../mathlib-ci/scripts/pr_summary/import_trans_difference.sh all
There are 6942 files with changed transitive imports taking up over 306424 characters: this is too many to display!
You can run this locally from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

---

Declarations diff (regex)

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean -- pending)

Computed after the build finishes.

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 49ac088e17
Reference commit b33266fe41

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/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).