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

[bryangingechen]

The initial commit was generated by running lake shake --add-public --keep-implied --keep-prefix --fix --explain > explain.txt at commit 325dc1f.

[github-actions]

PR summary 325dc1f0c5

Import changes exceeding 2%

%	File
+3.73%	Mathlib.Algebra.GroupWithZero.Units.Basic
+14.55%	Mathlib.Tactic.CongrExclamation
+3.57%	Mathlib.Tactic.FunProp.Types
+2.63%	Mathlib.Tactic.GRewrite.Elab
+33.33%	Mathlib.Tactic.Linter.Style
+200.00%	Mathlib.Tactic.Nontriviality.Core
+2.20%	Mathlib.Tactic.NormNum.Result
+3.77%	Mathlib.Tactic.SetLike
+367.27%	Mathlib.Tactic.Simproc.Divisors
+3.64%	Mathlib.Tactic.Simps.Basic

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Tactic.Simproc.Divisors	55	257	+202 (+367.27%)
Mathlib.Tactic.Nontriviality.Core	1	3	+2 (+200.00%)
Mathlib.Computability.TMComputable	996	256	-740 (-74.30%)
Mathlib.Computability.TMToPartrec	659	256	-403 (-61.15%)
Mathlib.Computability.TMConfig	638	256	-382 (-59.87%)
Mathlib.Order.Synonym	131	55	-76 (-58.02%)
Mathlib.Computability.PostTuringMachine	477	254	-223 (-46.75%)
Mathlib.InformationTheory.Coding.UniquelyDecodable	172	95	-77 (-44.77%)
Mathlib.AlgebraicTopology.SimplicialComplex.Basic	1071	623	-448 (-41.83%)
Mathlib.Logic.IsEmpty	86	54	-32 (-37.21%)
Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty	637	400	-237 (-37.21%)
Mathlib.Tactic.Linter.Style	3	4	+1 (+33.33%)
Mathlib.Computability.Tape	337	251	-86 (-25.52%)
Mathlib.Lean.Elab.InfoTree	8	6	-2 (-25.00%)
Mathlib.NumberTheory.NumberField.FinitePlaces	2977	2235	-742 (-24.92%)
Mathlib.Tactic.Linarith.NNRealPreprocessor	920	722	-198 (-21.52%)
Mathlib.Computability.StateTransition	462	363	-99 (-21.43%)
Mathlib.Algebra.Module.Torsion.PrimaryComponent	1720	1362	-358 (-20.81%)
Mathlib.Topology.Spectral.ConstructibleTopology	886	736	-150 (-16.93%)
Mathlib.Algebra.Group.Conj	346	295	-51 (-14.74%)
Mathlib.Tactic.CongrExclamation	55	63	+8 (+14.55%)
Mathlib.Order.Lex	129	112	-17 (-13.18%)
Mathlib.Analysis.ConstantSpeed	1597	1393	-204 (-12.77%)
Mathlib.Algebra.Module.Injective	1117	976	-141 (-12.62%)
Mathlib.Data.Nat.Cast.Synonym	141	124	-17 (-12.06%)
Mathlib.Order.ConditionallyCompletePartialOrder.Basic	248	222	-26 (-10.48%)
Mathlib.Data.Bool.Count	411	373	-38 (-9.25%)
Mathlib.MeasureTheory.Measure.CharacteristicFunction	2548	2320	-228 (-8.95%)
Mathlib.RingTheory.IntegralClosure.IntegralRestrict	1989	1826	-163 (-8.20%)
Mathlib.LinearAlgebra.LinearIndependent.BaseChange	1257	1154	-103 (-8.19%)
Mathlib.Analysis.Normed.Module.Bases	2017	1865	-152 (-7.54%)
Mathlib.Data.Int.Order.Basic	91	85	-6 (-6.59%)
Mathlib.Algebra.MvPolynomial.Cardinal	1201	1123	-78 (-6.49%)
Mathlib.LinearAlgebra.FixedSubmodule	1129	1056	-73 (-6.47%)
Mathlib.NumberTheory.ArithmeticFunction.LFunction	1505	1409	-96 (-6.38%)
Mathlib.Testing.Plausible.Sampleable	96	90	-6 (-6.25%)
Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset	612	574	-38 (-6.21%)
Mathlib.CategoryTheory.Adhesive.Subobject	952	899	-53 (-5.57%)
Mathlib.Order.GaloisConnection.Defs	164	155	-9 (-5.49%)
Mathlib.RingTheory.DedekindDomain.Factorization	2012	1914	-98 (-4.87%)
Mathlib.Data.List.DropRight	276	263	-13 (-4.71%)
Mathlib.Data.List.Forall2	265	253	-12 (-4.53%)
Mathlib.Algebra.Homology.ModelCategory.Lifting	1288	1233	-55 (-4.27%)
Mathlib.Data.List.Perm.Basic	269	258	-11 (-4.09%)
Mathlib.Tactic.SetLike	53	55	+2 (+3.77%)
Mathlib.Algebra.GroupWithZero.Units.Basic	134	139	+5 (+3.73%)
Mathlib.Analysis.Calculus.FDeriv.Affine	1732	1669	-63 (-3.64%)
Mathlib.Tactic.Simps.Basic	55	57	+2 (+3.64%)
Mathlib.Tactic.FunProp.Types	56	58	+2 (+3.57%)
Mathlib.Algebra.Group.Submonoid.Support	655	632	-23 (-3.51%)
Mathlib.CategoryTheory.Sites.Over	1071	1035	-36 (-3.36%)
Mathlib.LinearAlgebra.TensorProduct.Defs	807	780	-27 (-3.35%)
Mathlib.LinearAlgebra.SModEq.Pow	1170	1131	-39 (-3.33%)
Mathlib.Computability.TuringMachine.Config	637	617	-20 (-3.14%)
Mathlib.Algebra.Regular.Defs	65	63	-2 (-3.08%)
Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule	2478	2403	-75 (-3.03%)
Mathlib.CategoryTheory.Triangulated.TStructure.Heart	1121	1091	-30 (-2.68%)
Mathlib.Tactic.GRewrite.Elab	76	78	+2 (+2.63%)
Mathlib.Analysis.InnerProductSpace.Positive	2454	2398	-56 (-2.28%)
Mathlib.Tactic.NormNum.Result	182	186	+4 (+2.20%)
Mathlib.Data.List.Sigma	282	276	-6 (-2.13%)
Mathlib.Tactic.DSimpPercent	52	53	+1 (+1.92%)
Mathlib.Tactic.Peel	260	265	+5 (+1.92%)
Mathlib.Data.Nat.Cast.WithTop	211	207	-4 (-1.90%)
Mathlib.Data.Finset.Attr	53	54	+1 (+1.89%)
Mathlib.Tactic.Linter.FindDeprecations	53	52	-1 (-1.89%)
Mathlib.Logic.Equiv.PartialEquiv	214	218	+4 (+1.87%)
Mathlib.Tactic.Attr.Core	55	56	+1 (+1.82%)
Mathlib.Tactic.Tauto	55	56	+1 (+1.82%)
Mathlib.Data.Set.Dissipate	575	565	-10 (-1.74%)
Mathlib.Tactic.Hint	58	57	-1 (-1.72%)
Mathlib.CategoryTheory.Monoidal.Internal.Limits	473	465	-8 (-1.69%)
Mathlib.Tactic.Widget.Calc	61	60	-1 (-1.64%)
Mathlib.Tactic.Widget.InteractiveUnfold	61	60	-1 (-1.64%)
Mathlib.AlgebraicGeometry.Noetherian	2413	2374	-39 (-1.62%)
Mathlib.Tactic.Widget.Conv	63	62	-1 (-1.59%)
Mathlib.Algebra.MvPolynomial.Division	1077	1060	-17 (-1.58%)
Mathlib.CategoryTheory.Sites.SheafCohomology.Basic	1760	1733	-27 (-1.53%)
Mathlib.Order.Defs.PartialOrder	67	66	-1 (-1.49%)
Mathlib.Order.Notation	68	67	-1 (-1.47%)
Mathlib.Data.Set.Image	207	210	+3 (+1.45%)
Mathlib.Data.Set.Prod	209	212	+3 (+1.44%)
Mathlib.SetTheory.Cardinal.Defs	142	144	+2 (+1.41%)
Mathlib.RingTheory.AlgebraicIndependent.Defs	1074	1059	-15 (-1.40%)
Mathlib.Data.Nat.WithBot	215	218	+3 (+1.40%)
Mathlib.GroupTheory.FreeGroup.Basic	434	428	-6 (-1.38%)
Mathlib.Tactic.GRewrite.Core	75	76	+1 (+1.33%)
Mathlib.Order.Defs.LinearOrder	76	77	+1 (+1.32%)
Mathlib.Probability.Distributions.Gaussian.CharFun	2866	2829	-37 (-1.29%)
Mathlib.Tactic.Widget.StringDiagram	318	322	+4 (+1.26%)
Mathlib.LinearAlgebra.Transvection.Basic	1706	1685	-21 (-1.23%)
Mathlib.Order.Cofinal	247	250	+3 (+1.21%)
Mathlib.SetTheory.Cardinal.Embedding	757	748	-9 (-1.19%)
Mathlib.Tactic.Sat.FromLRAT	86	87	+1 (+1.16%)
Mathlib.AlgebraicGeometry.Modules.Tilde	2331	2304	-27 (-1.16%)
Mathlib.Data.SetLike.Basic	174	176	+2 (+1.15%)
Mathlib.Data.Prod.Basic	88	87	-1 (-1.14%)
Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered	1161	1148	-13 (-1.12%)
Mathlib.Data.Option.Basic	91	90	-1 (-1.10%)
Mathlib.Order.Filter.AtTopBot.CompleteLattice	279	282	+3 (+1.08%)
Mathlib.LinearAlgebra.Matrix.MvPolynomial	1276	1263	-13 (-1.02%)
Mathlib.Algebra.Module.SpanRank	1299	1286	-13 (-1.00%)
Mathlib.Algebra.Order.Group.Indicator	304	307	+3 (+0.99%)
Mathlib.RingTheory.LocalProperties.InjectiveDimension	2092	2072	-20 (-0.96%)
Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution	1273	1261	-12 (-0.94%)
Mathlib.RingTheory.RegularLocalRing.Defs	2153	2133	-20 (-0.93%)
Mathlib.AlgebraicTopology.SimplicialSet.Monoidal	973	964	-9 (-0.92%)
Mathlib.Order.Basic	109	110	+1 (+0.92%)
Mathlib.CategoryTheory.Monoidal.Widesubcategory	484	480	-4 (-0.83%)
Mathlib.RingTheory.FreeCommRing	1185	1176	-9 (-0.76%)
Mathlib.RingTheory.Polynomial.SmallDegreeVieta	1338	1328	-10 (-0.75%)
Mathlib.LinearAlgebra.TensorProduct.Basic	808	802	-6 (-0.74%)
Mathlib.Data.List.Zip	273	275	+2 (+0.73%)
Mathlib.GroupTheory.GroupAction.MultipleTransitivity	1104	1096	-8 (-0.72%)
Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM	1522	1511	-11 (-0.72%)
Mathlib.CategoryTheory.Abelian.Preradical.Colon	834	828	-6 (-0.72%)
Mathlib.Logic.Embedding.Basic	142	143	+1 (+0.70%)
Mathlib.Data.Set.Finite.Basic	427	430	+3 (+0.70%)
Mathlib.Algebra.Category.Ring.Topology	1605	1594	-11 (-0.69%)
Mathlib.Data.Ordmap.Ordnode	149	150	+1 (+0.67%)
Mathlib.Algebra.MvPolynomial.Funext	1242	1234	-8 (-0.64%)
Mathlib.RingTheory.MvPolynomial.Symmetric.Defs	1096	1089	-7 (-0.64%)
Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities	1097	1090	-7 (-0.64%)
Mathlib.GroupTheory.GroupAction.MultiplePrimitivity	1105	1098	-7 (-0.63%)
Mathlib.Order.Monotone.Basic	158	159	+1 (+0.63%)
Mathlib.Data.Set.Countable	476	479	+3 (+0.63%)
Mathlib.Algebra.Group.Int.Even	320	318	-2 (-0.62%)
Mathlib.MeasureTheory.MeasurableSpace.Defs	483	486	+3 (+0.62%)
Mathlib.RingTheory.RingHom.FiniteType	1638	1628	-10 (-0.61%)
Mathlib.Topology.Order	495	498	+3 (+0.61%)
Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss	2479	2464	-15 (-0.61%)
Mathlib.RingTheory.RingHom.FinitePresentation	1834	1823	-11 (-0.60%)
Mathlib.Data.Set.Basic	171	172	+1 (+0.58%)
Mathlib.Data.Bundle	172	173	+1 (+0.58%)
Mathlib.Data.Fin.Parity	520	523	+3 (+0.58%)
Mathlib.Analysis.SpecialFunctions.Stirling	2481	2467	-14 (-0.56%)
Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis	2309	2296	-13 (-0.56%)
Mathlib.RingTheory.MvPowerSeries.Evaluation	1429	1421	-8 (-0.56%)
Mathlib.Algebra.Group.UniqueProds.Basic	557	560	+3 (+0.54%)
Mathlib.Data.Fintype.Order	559	562	+3 (+0.54%)
Mathlib.RingTheory.MvPolynomial.Localization	1322	1315	-7 (-0.53%)
Mathlib.Order.PartialSups	572	575	+3 (+0.52%)
Mathlib.Analysis.Complex.Harmonic.Poisson	2516	2503	-13 (-0.52%)
Mathlib.Order.WellFoundedSet	584	587	+3 (+0.51%)
Mathlib.Analysis.Distribution.SchwartzSpace.Basic	2543	2530	-13 (-0.51%)
Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus	2351	2339	-12 (-0.51%)
Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected	589	592	+3 (+0.51%)
Mathlib.MeasureTheory.MeasurableSpace.Basic	589	592	+3 (+0.51%)
Mathlib.Order.Disjointed	596	599	+3 (+0.50%)
Mathlib.Data.TypeVec	398	400	+2 (+0.50%)
Mathlib.Topology.OpenPartialHomeomorph.Defs	612	615	+3 (+0.49%)
Mathlib.Topology.List	617	620	+3 (+0.49%)
Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional	1453	1446	-7 (-0.48%)
Mathlib.Data.Fintype.Basic	416	418	+2 (+0.48%)
Mathlib.LinearAlgebra.Matrix.FixedDetMatrices	1460	1453	-7 (-0.48%)
Mathlib.Geometry.Manifold.Complex	2515	2503	-12 (-0.48%)
Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique	2524	2512	-12 (-0.48%)
Mathlib.LinearAlgebra.Matrix.Hermitian	1482	1475	-7 (-0.47%)
Mathlib.Algebra.BigOperators.Intervals	642	645	+3 (+0.47%)
Mathlib.RingTheory.MvPolynomial.Homogeneous	1285	1279	-6 (-0.47%)
Mathlib.Analysis.Complex.JensenFormula	2578	2566	-12 (-0.47%)
Mathlib.Combinatorics.Compactness	652	655	+3 (+0.46%)
Mathlib.Algebra.Order.BigOperators.Ring.List	435	437	+2 (+0.46%)
Mathlib.CategoryTheory.Limits.Constructions.WidePullbackOfTerminal	439	437	-2 (-0.46%)
Mathlib.RingTheory.Polynomial.Basic	1318	1312	-6 (-0.46%)
Mathlib.Algebra.Polynomial.Sequence	1319	1313	-6 (-0.45%)
Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Terminal	441	439	-2 (-0.45%)
Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic	1554	1547	-7 (-0.45%)
Mathlib.Analysis.Complex.UpperHalfPlane.Manifold	2674	2662	-12 (-0.45%)
Mathlib.NumberTheory.Height.MvPolynomial	1793	1785	-8 (-0.45%)
Mathlib.LinearAlgebra.QuadraticForm.Radical	1569	1562	-7 (-0.45%)
Mathlib.LinearAlgebra.QuadraticForm.Signature	1570	1563	-7 (-0.45%)
Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable	2701	2689	-12 (-0.44%)
Mathlib.NumberTheory.ModularForms.Basic	2709	2697	-12 (-0.44%)
Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic	1355	1349	-6 (-0.44%)
Mathlib.FieldTheory.Minpoly.Basic	1356	1350	-6 (-0.44%)
Mathlib.LinearAlgebra.Matrix.PosDef	1587	1580	-7 (-0.44%)
Mathlib.Geometry.Manifold.WhitneyEmbedding	2504	2493	-11 (-0.44%)
Mathlib.Data.Nat.Choose.Lucas	1370	1364	-6 (-0.44%)
Mathlib.Algebra.Algebra.Subalgebra.Rank	1373	1367	-6 (-0.44%)
Mathlib.RingTheory.MvPolynomial	1386	1380	-6 (-0.43%)
Mathlib.NumberTheory.RamificationInertia.Unramified	2313	2303	-10 (-0.43%)
Mathlib.RingTheory.Algebraic.Basic	1397	1391	-6 (-0.43%)
Mathlib.NumberTheory.FLT.Polynomial	1404	1398	-6 (-0.43%)
Mathlib.LinearAlgebra.LinearDisjoint	1416	1410	-6 (-0.42%)
Mathlib.RingTheory.UniqueFactorizationDomain.Basic	709	712	+3 (+0.42%)
Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors	713	716	+3 (+0.42%)
Mathlib.Topology.LocallyConstant.Basic	716	719	+3 (+0.42%)
Mathlib.CategoryTheory.Shift.Adjunction	478	476	-2 (-0.42%)
Mathlib.Analysis.CStarAlgebra.Spectrum	2642	2631	-11 (-0.42%)
Mathlib.RingTheory.DedekindDomain.Instances	1923	1915	-8 (-0.42%)
Mathlib.Topology.OpenPartialHomeomorph.Basic	722	725	+3 (+0.42%)
Mathlib.Topology.OpenPartialHomeomorph.IsImage	724	727	+3 (+0.41%)
Mathlib.Topology.OpenPartialHomeomorph.Composition	725	728	+3 (+0.41%)
Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv	1452	1446	-6 (-0.41%)
Mathlib.Topology.OpenPartialHomeomorph.Constructions	726	729	+3 (+0.41%)
Mathlib.Data.Sym.Sym2	487	489	+2 (+0.41%)
Mathlib.FieldTheory.IsAlgClosed.Spectrum	1744	1737	-7 (-0.40%)
Mathlib.Data.List.Count	250	251	+1 (+0.40%)
Mathlib.Analysis.Complex.Schwarz	2501	2491	-10 (-0.40%)
Mathlib.Analysis.Complex.Harmonic.Liouville	2510	2500	-10 (-0.40%)
Mathlib.Data.List.ChainOfFn	252	253	+1 (+0.40%)
Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity	771	774	+3 (+0.39%)
Mathlib.Combinatorics.SimpleGraph.Hamiltonian	772	775	+3 (+0.39%)
Mathlib.ModelTheory.FinitelyGenerated	772	775	+3 (+0.39%)
Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant	2326	2317	-9 (-0.39%)
Mathlib.Dynamics.PeriodicPts.Defs	517	519	+2 (+0.39%)
Mathlib.RingTheory.DedekindDomain.Different	2346	2337	-9 (-0.38%)
Mathlib.Combinatorics.SimpleGraph.VertexCover	788	791	+3 (+0.38%)
Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology	1839	1832	-7 (-0.38%)
Mathlib.Data.List.Basic	263	264	+1 (+0.38%)
Mathlib.Tactic.ENatToNat	530	532	+2 (+0.38%)
Mathlib.Data.List.Nodup	266	267	+1 (+0.38%)
Mathlib.Data.Seq.Basic	537	539	+2 (+0.37%)
Mathlib.NumberTheory.DiophantineApproximation.Basic	1635	1629	-6 (-0.37%)
Mathlib.Data.NNRat.Lemmas	552	554	+2 (+0.36%)
Mathlib.NumberTheory.Pell	1670	1664	-6 (-0.36%)
Mathlib.Combinatorics.Additive.VerySmallDoubling	1685	1679	-6 (-0.36%)
Mathlib.NumberTheory.RatFunc.Ostrowski	2253	2245	-8 (-0.36%)
Mathlib.RingTheory.Localization.AtPrime.Extension	2004	1997	-7 (-0.35%)
Mathlib.RingTheory.Valuation.ValuativeRel.Basic	1161	1157	-4 (-0.34%)
Mathlib.Order.Filter.Subsingleton	585	587	+2 (+0.34%)
Mathlib.Analysis.Normed.Module.Dual	2070	2063	-7 (-0.34%)
Mathlib.Data.Fin.Basic	296	295	-1 (-0.34%)
Mathlib.Order.Filter.EventuallyConst	594	596	+2 (+0.34%)
Mathlib.Algebra.BigOperators.Group.List.Basic	298	299	+1 (+0.34%)
Mathlib.GroupTheory.OrderOfElement	912	915	+3 (+0.33%)
Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly	609	607	-2 (-0.33%)
Mathlib.Geometry.Manifold.Immersion	2143	2136	-7 (-0.33%)
Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic	2173	2166	-7 (-0.32%)
Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff	1554	1549	-5 (-0.32%)
Mathlib.RingTheory.IntegralClosure.Algebra.Basic	1563	1558	-5 (-0.32%)
Mathlib.Tactic.NormNum.Irrational	1886	1880	-6 (-0.32%)
Mathlib.LinearAlgebra.Determinant	1598	1593	-5 (-0.31%)
Mathlib.LinearAlgebra.FreeModule.Determinant	1599	1594	-5 (-0.31%)
Mathlib.LinearAlgebra.Matrix.Rank	1609	1604	-5 (-0.31%)
Mathlib.RingTheory.Polynomial.DegreeLT	1611	1606	-5 (-0.31%)
Mathlib.FieldTheory.IntermediateField.Algebraic	1623	1618	-5 (-0.31%)
Mathlib.RingTheory.PowerBasis	1623	1618	-5 (-0.31%)
Mathlib.RingTheory.Localization.Integral	1624	1619	-5 (-0.31%)
Mathlib.RingTheory.Adjoin.PowerBasis	1625	1620	-5 (-0.31%)
Mathlib.FieldTheory.Separable	1627	1622	-5 (-0.31%)
Mathlib.Combinatorics.SimpleGraph.Acyclic	977	980	+3 (+0.31%)
Mathlib.RingTheory.AdjoinRoot	1630	1625	-5 (-0.31%)
Mathlib.Algebra.Order.Archimedean.Basic	657	659	+2 (+0.30%)
Mathlib.RingTheory.Finiteness.Descent	1978	1972	-6 (-0.30%)
Mathlib.RingTheory.Valuation.Integral	1649	1644	-5 (-0.30%)
Mathlib.NumberTheory.NumberField.Completion.FinitePlace	2977	2968	-9 (-0.30%)
Mathlib.Combinatorics.SimpleGraph.ConcreteColorings	994	997	+3 (+0.30%)
Mathlib.RingTheory.IsAdjoinRoot	1671	1666	-5 (-0.30%)
Mathlib.LinearAlgebra.Charpoly.ToMatrix	1678	1673	-5 (-0.30%)
Mathlib.FieldTheory.IntermediateField.Adjoin.Basic	1679	1674	-5 (-0.30%)
Mathlib.LinearAlgebra.Charpoly.BaseChange	1680	1675	-5 (-0.30%)
Mathlib.LinearAlgebra.SpecialLinearGroup	1681	1676	-5 (-0.30%)
Mathlib.RingTheory.LinearDisjoint	1689	1684	-5 (-0.30%)
Mathlib.Data.Nat.Fib.Basic	677	679	+2 (+0.30%)
Mathlib.FieldTheory.Finite.Basic	1701	1696	-5 (-0.29%)
Mathlib.NumberTheory.SumFourSquares	1702	1697	-5 (-0.29%)
Mathlib.RingTheory.Polynomial.Resultant.Basic	1705	1700	-5 (-0.29%)
Mathlib.LinearAlgebra.Matrix.Charpoly.Disc	1706	1701	-5 (-0.29%)
Mathlib.NumberTheory.FermatPsp	1721	1716	-5 (-0.29%)
Mathlib.Algebra.Group.Fin.Basic	346	345	-1 (-0.29%)
Mathlib.FieldTheory.PrimitiveElement	1734	1729	-5 (-0.29%)
Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith	2083	2077	-6 (-0.29%)
Mathlib.RingTheory.Norm.Basic	1736	1731	-5 (-0.29%)
Mathlib.Analysis.Normed.Module.DoubleDual	2084	2078	-6 (-0.29%)
Mathlib.NumberTheory.SumTwoSquares	1741	1736	-5 (-0.29%)
Mathlib.FieldTheory.IsSepClosed	1742	1737	-5 (-0.29%)
Mathlib.RingTheory.Norm.Transitivity	1746	1741	-5 (-0.29%)
Mathlib.FieldTheory.Minpoly.MinpolyDiv	1747	1742	-5 (-0.29%)
Mathlib.Algebra.Module.Submodule.Invariant	700	702	+2 (+0.29%)
Mathlib.RingTheory.Ideal.Height	1770	1765	-5 (-0.28%)
Mathlib.Data.Nat.Factorial.BigOperators	712	714	+2 (+0.28%)
Mathlib.Geometry.Manifold.ContMDiff.Atlas	2142	2136	-6 (-0.28%)
Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions	2144	2138	-6 (-0.28%)
Mathlib.Geometry.Manifold.Algebra.Monoid	2147	2141	-6 (-0.28%)
Mathlib.Geometry.Manifold.Algebra.LieGroup	2148	2142	-6 (-0.28%)
Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable	2158	2152	-6 (-0.28%)
Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential	2159	2153	-6 (-0.28%)
Mathlib.Data.List.FinRange	360	359	-1 (-0.28%)
Mathlib.Algebra.Category.Ring.Limits	723	725	+2 (+0.28%)
Mathlib.Geometry.Manifold.VectorBundle.Tensoriality	2169	2163	-6 (-0.28%)
Mathlib.Topology.Compactness.CountablyCompact	723	725	+2 (+0.28%)
Mathlib.CategoryTheory.Sites.Hypercover.One	724	726	+2 (+0.28%)
Mathlib.GroupTheory.Perm.Basic	364	363	-1 (-0.27%)
Mathlib.Geometry.Manifold.VectorField.LieBracket	2187	2181	-6 (-0.27%)
Mathlib.Topology.Algebra.Valued.ValuativeRel	1840	1835	-5 (-0.27%)
Mathlib.CategoryTheory.Triangulated.Opposite.Basic	738	740	+2 (+0.27%)
Mathlib.MeasureTheory.Integral.Bochner.Basic	2234	2228	-6 (-0.27%)
Mathlib.Algebra.CharP.Defs	373	374	+1 (+0.27%)
Mathlib.Data.Vector.Basic	373	374	+1 (+0.27%)
Mathlib.Order.Interval.Finset.Box	749	751	+2 (+0.27%)
Mathlib.Geometry.Manifold.Instances.Icc	2250	2244	-6 (-0.27%)
Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet	757	759	+2 (+0.26%)
Mathlib.Algebra.Order.Ring.StandardPart	1927	1922	-5 (-0.26%)
Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction	2357	2351	-6 (-0.25%)
Mathlib.Order.Atoms	400	401	+1 (+0.25%)
Mathlib.Combinatorics.Schnirelmann	802	804	+2 (+0.25%)
Mathlib.LinearAlgebra.TensorProduct.Map	809	811	+2 (+0.25%)
Mathlib.Tactic.NormNum.Prime	405	404	-1 (-0.25%)
Mathlib.NumberTheory.Niven	2027	2022	-5 (-0.25%)
Mathlib.Combinatorics.Additive.SmallTripling	812	814	+2 (+0.25%)
Mathlib.Probability.Distributions.Binomial	2439	2433	-6 (-0.25%)
Mathlib.Analysis.AbsoluteValue.Equivalence	2036	2031	-5 (-0.25%)
Mathlib.Analysis.Convex.Approximation	2046	2041	-5 (-0.24%)
Mathlib.Data.Nat.Digits.Lemmas	822	824	+2 (+0.24%)
Mathlib.Tactic.CategoryTheory.Elementwise	411	410	-1 (-0.24%)
Mathlib.Tactic.CategoryTheory.ToApp	413	412	-1 (-0.24%)
Mathlib.Data.Nat.Choose.Sum	833	835	+2 (+0.24%)
Mathlib.Algebra.Group.Subgroup.Basic	417	418	+1 (+0.24%)
Mathlib.Topology.Order.Basic	843	845	+2 (+0.24%)
Mathlib.Algebra.Homology.HomologicalComplexAbelian	846	844	-2 (-0.24%)
Mathlib.Topology.Order.SuccPred	846	848	+2 (+0.24%)
Mathlib.Topology.Order.LeftRightNhds	849	851	+2 (+0.24%)
Mathlib.Data.Set.Card.Arithmetic	855	857	+2 (+0.23%)
Mathlib.Data.NNRat.Defs	430	431	+1 (+0.23%)
Mathlib.Topology.Order.Monotone	860	862	+2 (+0.23%)
Mathlib.Data.Real.CompleteField	1295	1292	-3 (-0.23%)
Mathlib.Topology.FiberBundle.Trivialization	885	887	+2 (+0.23%)
Mathlib.Analysis.Normed.Algebra.Spectrum	2230	2225	-5 (-0.22%)
Mathlib.Topology.FiberBundle.Basic	892	894	+2 (+0.22%)
Mathlib.Topology.FiberBundle.Constructions	893	895	+2 (+0.22%)
Mathlib.MeasureTheory.Group.Integral	2235	2230	-5 (-0.22%)
Mathlib.RingTheory.Nilpotent.Basic	894	896	+2 (+0.22%)
Mathlib.MeasureTheory.Measure.HasOuterApproxClosed	2244	2239	-5 (-0.22%)
Mathlib.MeasureTheory.Integral.Bochner.SumMeasure	2248	2243	-5 (-0.22%)
Mathlib.Topology.Algebra.InfiniteSum.Basic	908	910	+2 (+0.22%)
Mathlib.Data.Multiset.Functor	456	457	+1 (+0.22%)
Mathlib.Data.Nat.Choose.Factorization	915	917	+2 (+0.22%)
Mathlib.Data.Nat.Multiplicity	916	918	+2 (+0.22%)
Mathlib.Data.NNReal.Basic	919	921	+2 (+0.22%)
Mathlib.Algebra.Squarefree.Basic	921	923	+2 (+0.22%)
Mathlib.RingTheory.Radical.Basic	926	928	+2 (+0.22%)
Mathlib.Analysis.Calculus.LogDeriv	1868	1864	-4 (-0.21%)
Mathlib.MeasureTheory.Measure.TightNormed	2344	2339	-5 (-0.21%)
Mathlib.Tactic.PNatToNat	470	471	+1 (+0.21%)
Mathlib.Probability.Distributions.TwoValued	2366	2361	-5 (-0.21%)
Mathlib.LinearAlgebra.Basis.Flag	955	957	+2 (+0.21%)
Mathlib.NumberTheory.Primorial	959	961	+2 (+0.21%)
Mathlib.Data.Matrix.Basis	960	962	+2 (+0.21%)
Mathlib.CategoryTheory.CopyDiscardCategory.Widesubcategory	485	484	-1 (-0.21%)
Mathlib.LinearAlgebra.LinearIndependent.Lemmas	986	988	+2 (+0.20%)
Mathlib.GroupTheory.GroupAction.Primitive	987	989	+2 (+0.20%)
Mathlib.LinearAlgebra.Matrix.DotProduct	992	994	+2 (+0.20%)
Mathlib.LinearAlgebra.Ray	997	999	+2 (+0.20%)
Mathlib.Tactic.Positivity.Basic	505	504	-1 (-0.20%)
Mathlib.GroupTheory.Coxeter.Basic	1013	1015	+2 (+0.20%)
Mathlib.Algebra.Order.Field.Power	508	507	-1 (-0.20%)
Mathlib.LinearAlgebra.Dimension.Basic	1016	1018	+2 (+0.20%)
Mathlib.LinearAlgebra.Dimension.Subsingleton	1017	1019	+2 (+0.20%)
Mathlib.Data.Nat.Totient	1025	1027	+2 (+0.20%)
Mathlib.NumberTheory.Multiplicity	1028	1030	+2 (+0.19%)
Mathlib.Algebra.Polynomial.Eval.Coeff	1029	1031	+2 (+0.19%)
Mathlib.Algebra.Polynomial.Degree.Operations	1038	1040	+2 (+0.19%)
Mathlib.Algebra.Polynomial.Degree.TrailingDegree	1042	1044	+2 (+0.19%)
Mathlib.Algebra.Polynomial.Degree.Units	1042	1044	+2 (+0.19%)
Mathlib.Topology.MetricSpace.Bounded	1042	1044	+2 (+0.19%)
Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs	1043	1045	+2 (+0.19%)
Mathlib.Algebra.Polynomial.Derivative	1044	1046	+2 (+0.19%)
Mathlib.RingTheory.Polynomial.Opposites	1044	1046	+2 (+0.19%)
Mathlib.Algebra.Polynomial.Degree.Lemmas	1047	1049	+2 (+0.19%)
Mathlib.Topology.MetricSpace.Antilipschitz	1048	1050	+2 (+0.19%)
Mathlib.Analysis.Convex.Extreme	1051	1053	+2 (+0.19%)
Mathlib.Topology.MetricSpace.Isometry	1051	1053	+2 (+0.19%)
Mathlib.Algebra.MvPolynomial.Basic	1054	1056	+2 (+0.19%)
Mathlib.Algebra.Polynomial.EraseLead	1054	1056	+2 (+0.19%)
Mathlib.Topology.MetricSpace.Dilation	1056	1058	+2 (+0.19%)
Mathlib.Topology.MetricSpace.Congruence	1057	1059	+2 (+0.19%)
Mathlib.Algebra.Polynomial.Reverse	1058	1060	+2 (+0.19%)
Mathlib.Algebra.Polynomial.Mirror	1059	1061	+2 (+0.19%)
Mathlib.Algebra.Polynomial.Monic	1059	1061	+2 (+0.19%)
Mathlib.Topology.MetricSpace.Similarity	1059	1061	+2 (+0.19%)
Mathlib.Algebra.Polynomial.BigOperators	1062	1064	+2 (+0.19%)
Mathlib.Algebra.Polynomial.UnitTrinomial	1062	1064	+2 (+0.19%)
Mathlib.Algebra.Polynomial.Div	1064	1066	+2 (+0.19%)
Mathlib.Combinatorics.SimpleGraph.FiveWheelLike	1064	1066	+2 (+0.19%)
Mathlib.Geometry.Manifold.StructureGroupoid	1066	1068	+2 (+0.19%)
Mathlib.NumberTheory.MulChar.Basic	1070	1072	+2 (+0.19%)
Mathlib.GroupTheory.SpecificGroups.Alternating	1074	1076	+2 (+0.19%)
Mathlib.GroupTheory.CommutingProbability	1093	1095	+2 (+0.18%)
Mathlib.Algebra.Polynomial.PartialFractions	1096	1098	+2 (+0.18%)
Mathlib.Analysis.Normed.Group.Basic	1100	1102	+2 (+0.18%)
Mathlib.AlgebraicTopology.DoldKan.Degeneracies	1107	1109	+2 (+0.18%)
Mathlib.RingTheory.Nilpotent.Exp	1139	1141	+2 (+0.18%)
Mathlib.RingTheory.Polynomial.ShiftedLegendre	1143	1145	+2 (+0.17%)
Mathlib.GroupTheory.Coxeter.Length	1151	1153	+2 (+0.17%)
Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree	1153	1155	+2 (+0.17%)
Mathlib.GroupTheory.Sylow	1164	1166	+2 (+0.17%)
Mathlib.Algebra.Polynomial.Taylor	1174	1176	+2 (+0.17%)
Mathlib.Analysis.Convex.FunctionTopology	1174	1176	+2 (+0.17%)
Mathlib.RingTheory.Idempotents	1181	1183	+2 (+0.17%)
Mathlib.NumberTheory.PellMatiyasevic	1188	1190	+2 (+0.17%)
Mathlib.Algebra.Polynomial.Laurent	1198	1200	+2 (+0.17%)
Mathlib.Tactic.Rify	601	602	+1 (+0.17%)
Mathlib.Algebra.Azumaya.Matrix	1205	1207	+2 (+0.17%)
Mathlib.NumberTheory.Zsqrtd.GaussianInt	1216	1218	+2 (+0.16%)
Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas	613	614	+1 (+0.16%)
Mathlib.Data.Nat.Digits.Defs	616	617	+1 (+0.16%)
Mathlib.Analysis.Asymptotics.Defs	1235	1237	+2 (+0.16%)
Mathlib.Data.Nat.Choose.Central	620	621	+1 (+0.16%)
Mathlib.NumberTheory.EllipticDivisibilitySequence	632	633	+1 (+0.16%)
Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete	1281	1283	+2 (+0.16%)
Mathlib.RingTheory.Polynomial.Content	1283	1285	+2 (+0.16%)
Mathlib.RingTheory.MvPolynomial.MonomialOrder	1293	1295	+2 (+0.15%)
Mathlib.Algebra.MvPolynomial.NoZeroDivisors	1297	1299	+2 (+0.15%)
Mathlib.Algebra.Polynomial.Splits	1299	1301	+2 (+0.15%)
Mathlib.RingTheory.Polynomial.ScaleRoots	1300	1302	+2 (+0.15%)
Mathlib.Algebra.CubicDiscriminant	1301	1303	+2 (+0.15%)
Mathlib.RingTheory.Polynomial.IntegralNormalization	1301	1303	+2 (+0.15%)
Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion	2626	2622	-4 (-0.15%)
Mathlib.LinearAlgebra.Dimension.Finite	1317	1319	+2 (+0.15%)
Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition	1317	1319	+2 (+0.15%)
Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots	1317	1319	+2 (+0.15%)
Mathlib.NumberTheory.Harmonic.EulerMascheroni	1977	1974	-3 (-0.15%)
Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits	1318	1320	+2 (+0.15%)
Mathlib.RingTheory.Polynomial.Eisenstein.Basic	1321	1323	+2 (+0.15%)
Mathlib.Analysis.SpecialFunctions.BinaryEntropy	1983	1980	-3 (-0.15%)
Mathlib.Algebra.LinearRecurrence	1327	1329	+2 (+0.15%)
Mathlib.RingTheory.KrullDimension.Basic	1333	1335	+2 (+0.15%)
Mathlib.NumberTheory.FrobeniusNumber	1359	1361	+2 (+0.15%)
Mathlib.Algebra.MonoidAlgebra.Defs	682	683	+1 (+0.15%)
Mathlib.RingTheory.Henselian	1364	1366	+2 (+0.15%)
Mathlib.LinearAlgebra.Projectivization.Cardinality	1365	1367	+2 (+0.15%)
Mathlib.LinearAlgebra.Eigenspace.Basic	1367	1369	+2 (+0.15%)
Mathlib.Algebra.MvPolynomial.Nilpotent	1373	1375	+2 (+0.15%)
Mathlib.Analysis.Convex.StdSimplex	1377	1379	+2 (+0.15%)
Mathlib.RingTheory.MvPolynomial.Ideal	1379	1381	+2 (+0.15%)
Mathlib.Topology.CWComplex.Classical.Finite	1404	1406	+2 (+0.14%)
Mathlib.RingTheory.PowerSeries.PiTopology	1420	1422	+2 (+0.14%)
Mathlib.Combinatorics.Enumerative.Partition.GenFun	1423	1425	+2 (+0.14%)
Mathlib.Analysis.Normed.Operator.Conformal	1430	1432	+2 (+0.14%)
Mathlib.Combinatorics.Enumerative.Partition.Glaisher	1439	1441	+2 (+0.14%)
Mathlib.Analysis.LocallyConvex.Bounded	1446	1448	+2 (+0.14%)
Mathlib.MeasureTheory.Measure.NullMeasurable	1480	1482	+2 (+0.14%)
Mathlib.MeasureTheory.Measure.MeasureSpace	1484	1486	+2 (+0.13%)
Mathlib.CategoryTheory.Sites.Hypercover.Saturate	746	747	+1 (+0.13%)
Mathlib.MeasureTheory.Measure.Typeclasses.Finite	1492	1494	+2 (+0.13%)
Mathlib.MeasureTheory.Measure.Decomposition.Hahn	1493	1495	+2 (+0.13%)
Mathlib.NumberTheory.FunctionField	2243	2240	-3 (-0.13%)
Mathlib.Algebra.BigOperators.Finprod	749	750	+1 (+0.13%)
Mathlib.MeasureTheory.Measure.AEMeasurable	1498	1500	+2 (+0.13%)
Mathlib.Dynamics.Ergodic.MeasurePreserving	1501	1503	+2 (+0.13%)
Mathlib.Analysis.CStarAlgebra.Basic	1502	1504	+2 (+0.13%)
Mathlib.LinearAlgebra.Vandermonde	1503	1505	+2 (+0.13%)
Mathlib.MeasureTheory.Constructions.BorelSpace.Order	1506	1508	+2 (+0.13%)
Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan	1510	1508	-2 (-0.13%)
Mathlib.MeasureTheory.Measure.Stieltjes	1517	1515	-2 (-0.13%)
Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap	1523	1525	+2 (+0.13%)
Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity	1540	1542	+2 (+0.13%)
Mathlib.MeasureTheory.Constructions.Polish.Basic	1557	1559	+2 (+0.13%)
Mathlib.Analysis.SpecificLimits.Normed	1565	1567	+2 (+0.13%)
Mathlib.InformationTheory.Coding.KraftMcMillan	1567	1569	+2 (+0.13%)
Mathlib.Probability.Kernel.Defs	1569	1571	+2 (+0.13%)
Mathlib.Analysis.Real.OfDigits	1570	1572	+2 (+0.13%)
Mathlib.Analysis.Normed.Ring.Units	1574	1576	+2 (+0.13%)
Mathlib.Probability.Independence.Kernel.Indep	1578	1580	+2 (+0.13%)
Mathlib.RingTheory.Extension.Presentation.Basic	1585	1587	+2 (+0.13%)
Mathlib.Analysis.RCLike.Basic	1586	1588	+2 (+0.13%)
Mathlib.CategoryTheory.Sites.Continuous	793	794	+1 (+0.13%)
Mathlib.Analysis.RCLike.Extend	1587	1589	+2 (+0.13%)
Mathlib.Probability.UniformOn	1598	1600	+2 (+0.13%)
Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic	1601	1603	+2 (+0.12%)
Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable	1602	1604	+2 (+0.12%)
Mathlib.NumberTheory.Padics.PadicIntegers	1612	1614	+2 (+0.12%)
Mathlib.Analysis.Normed.Operator.Basic	1644	1646	+2 (+0.12%)
Mathlib.Analysis.Normed.Operator.NNNorm	1645	1647	+2 (+0.12%)
Mathlib.Probability.Independence.Kernel.IndepFun	1664	1666	+2 (+0.12%)
Mathlib.Analysis.Calculus.FDeriv.Const	1665	1667	+2 (+0.12%)
Mathlib.Analysis.Normed.Module.Alternating.Basic	1667	1669	+2 (+0.12%)
Mathlib.Probability.Independence.Basic	1673	1675	+2 (+0.12%)
Mathlib.LinearAlgebra.Basis.Defs	847	848	+1 (+0.12%)
Mathlib.LinearAlgebra.LinearIndependent.Defs	847	848	+1 (+0.12%)
Mathlib.FieldTheory.ChevalleyWarning	1702	1704	+2 (+0.12%)
Mathlib.Analysis.Analytic.OfScalars	1710	1712	+2 (+0.12%)
Mathlib.Analysis.Analytic.Basic	1711	1713	+2 (+0.12%)
Mathlib.Analysis.Analytic.Linear	1714	1716	+2 (+0.12%)
Mathlib.Analysis.Complex.AbelLimit	1716	1718	+2 (+0.12%)
Mathlib.Analysis.Normed.Module.RCLike.Basic	1719	1721	+2 (+0.12%)
Mathlib.FieldTheory.Finite.Polynomial	1720	1722	+2 (+0.12%)
Mathlib.Topology.VectorBundle.Basic	1722	1724	+2 (+0.12%)
Mathlib.Topology.VectorBundle.Hom	1723	1725	+2 (+0.12%)
Mathlib.Topology.VectorBundle.Constructions	1725	1727	+2 (+0.12%)
Mathlib.Analysis.Calculus.Conformal.NormedSpace	1731	1733	+2 (+0.12%)
Mathlib.RingTheory.WittVector.IsPoly	1731	1733	+2 (+0.12%)
Mathlib.RingTheory.WittVector.Verschiebung	1732	1734	+2 (+0.12%)
Mathlib.RingTheory.WittVector.Frobenius	1733	1735	+2 (+0.12%)
Mathlib.NumberTheory.Height.Basic	1736	1738	+2 (+0.12%)
Mathlib.RingTheory.WittVector.Identities	1736	1738	+2 (+0.12%)
Mathlib.Analysis.SpecialFunctions.Pow.NNReal	1772	1774	+2 (+0.11%)
Mathlib.Analysis.Asymptotics.SpecificAsymptotics	1776	1778	+2 (+0.11%)
Mathlib.Analysis.PSeries	1776	1778	+2 (+0.11%)
Mathlib.LinearAlgebra.LinearIndependent.Basic	889	890	+1 (+0.11%)
Mathlib.Topology.LocallyFinsupp	889	890	+1 (+0.11%)
Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk	1802	1804	+2 (+0.11%)
Mathlib.Combinatorics.SimpleGraph.Regularity.Increment	1804	1806	+2 (+0.11%)
Mathlib.Combinatorics.SimpleGraph.Triangle.Removal	1831	1833	+2 (+0.11%)
Mathlib.Analysis.Normed.Field.Approximation	1832	1834	+2 (+0.11%)
Mathlib.SetTheory.Ordinal.Topology	916	917	+1 (+0.11%)
Mathlib.RingTheory.RootsOfUnity.Complex	1846	1848	+2 (+0.11%)
Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity	1869	1871	+2 (+0.11%)
Mathlib.Probability.Distributions.Gaussian.Multivariate	2870	2867	-3 (-0.10%)
Mathlib.Analysis.Complex.CanonicalDecomposition	1984	1982	-2 (-0.10%)
Mathlib.CategoryTheory.MorphismProperty.CommaSites	1077	1078	+1 (+0.09%)
Mathlib.CategoryTheory.Sites.Descent.Precoverage	1083	1084	+1 (+0.09%)
Mathlib.NumberTheory.ClassNumber.Finite	2214	2216	+2 (+0.09%)
Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem	1115	1116	+1 (+0.09%)
Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed	2308	2306	-2 (-0.09%)
Mathlib.Algebra.MvPolynomial.Equiv	1164	1165	+1 (+0.09%)
Mathlib.Topology.Sheaves.Points	1175	1176	+1 (+0.09%)
Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc	1193	1194	+1 (+0.08%)
Mathlib.RingTheory.PowerSeries.Basic	1193	1194	+1 (+0.08%)
Mathlib.Algebra.Homology.DerivedCategory.Ext.Map	1411	1410	-1 (-0.07%)
Mathlib.RingTheory.AlgebraicIndependent.Transcendental	1415	1416	+1 (+0.07%)
Mathlib.Analysis.Asymptotics.TVS	1510	1511	+1 (+0.07%)
Mathlib.RingTheory.Polynomial.IsIntegral	1656	1657	+1 (+0.06%)
Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis	1662	1663	+1 (+0.06%)
Mathlib.Algebra.Module.LinearMap.Polynomial	1695	1696	+1 (+0.06%)
Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure	1747	1748	+1 (+0.06%)
Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point	1754	1755	+1 (+0.06%)
Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree	1758	1759	+1 (+0.06%)
Mathlib.FieldTheory.SeparableDegree	1769	1770	+1 (+0.06%)
Mathlib.Analysis.Calculus.ContDiff.Basic	1770	1771	+1 (+0.06%)
Mathlib.FieldTheory.PurelyInseparable.Basic	1779	1780	+1 (+0.06%)
Mathlib.Analysis.Calculus.ContDiff.Operations	1791	1792	+1 (+0.06%)
Mathlib.Geometry.Manifold.IsManifold.Basic	1860	1861	+1 (+0.05%)
Mathlib.RingTheory.KrullDimension.Module	1951	1950	-1 (-0.05%)
Mathlib.RingTheory.Valuation.Discrete.Basic	2238	2239	+1 (+0.04%)
Mathlib.AlgebraicGeometry.EllipticCurve.Reduction	2248	2249	+1 (+0.04%)
Mathlib.RingTheory.LaurentSeries	2270	2271	+1 (+0.04%)
Mathlib.AlgebraicGeometry.Morphisms.Finite	2333	2332	-1 (-0.04%)
Mathlib.RingTheory.Polynomial.Cyclotomic.Basic	2480	2481	+1 (+0.04%)
Mathlib.NumberTheory.Cyclotomic.Basic	2494	2495	+1 (+0.04%)
Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral	2495	2496	+1 (+0.04%)
Mathlib.RingTheory.Polynomial.Cyclotomic.Eval	2558	2559	+1 (+0.04%)
Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale	2658	2659	+1 (+0.04%)
Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder	2695	2694	-1 (-0.04%)

Import changes for all files

Files	Import difference
There are 7158 files with changed transitive imports taking up over 315906 characters: this is too many to display!
You can run ci-tools/scripts/pr_summary/import_trans_difference.sh all locally to see the whole output.

---

Declarations diff

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

You can run this locally as follows

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

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

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

---

No changes to technical debt.

You can run this locally as

./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).

[bryangingechen]

shake-explain.txt

Here's the output of --explain for this run.

[mathlib-merge-conflicts]

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