chore(GroupTheory/Index): don't import Field

[YaelDillies]

---

• depends on: chore(GroupTheory/Commutator): don't import Ring #21296

[github-actions]

PR summary 8c94e165da

Import changes exceeding 2%

%	File
+3.11%	Mathlib.GroupTheory.Commutator.Finite

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.GroupTheory.Commutator.Basic	572	451	-121 (-21.15%)
Mathlib.CategoryTheory.Action.Concrete	827	750	-77 (-9.31%)
Mathlib.GroupTheory.Abelianization	812	770	-42 (-5.17%)
Mathlib.GroupTheory.Index	831	789	-42 (-5.05%)
Mathlib.GroupTheory.Commutator.Finite	772	796	+24 (+3.11%)
Mathlib.GroupTheory.OrderOfElement	889	880	-9 (-1.01%)
Mathlib.NumberTheory.LucasLehmer	910	908	-2 (-0.22%)
Mathlib.GroupTheory.Perm.Cycle.Factors	918	916	-2 (-0.22%)
Mathlib.GroupTheory.Perm.ConjAct	922	920	-2 (-0.22%)
Mathlib.GroupTheory.Exponent	950	948	-2 (-0.21%)
Mathlib.GroupTheory.Coxeter.Inversion	1042	1040	-2 (-0.19%)
Mathlib.MeasureTheory.Measure.EverywherePos	1487	1485	-2 (-0.13%)
Mathlib.GroupTheory.Perm.Centralizer	958	957	-1 (-0.10%)
Mathlib.Topology.Algebra.Group.TopologicalAbelianization	1008	1007	-1 (-0.10%)
Mathlib.GroupTheory.Schreier	1198	1199	+1 (+0.08%)
Mathlib.MeasureTheory.Measure.Haar.Unique	2006	2005	-1 (-0.05%)

Import changes for all files

Files	Import difference
Mathlib.GroupTheory.Commutator.Basic	-121
Mathlib.CategoryTheory.Action.Concrete Mathlib.GroupTheory.GroupAction.Quotient	-77
11 files Mathlib.CategoryTheory.Action Mathlib.GroupTheory.Abelianization Mathlib.GroupTheory.Commensurable Mathlib.GroupTheory.Complement Mathlib.GroupTheory.FreeGroup.NielsenSchreier Mathlib.GroupTheory.GroupAction.CardCommute Mathlib.GroupTheory.GroupExtension.Defs Mathlib.GroupTheory.Index Mathlib.GroupTheory.PushoutI Mathlib.GroupTheory.SemidirectProduct Mathlib.GroupTheory.Solvable	-42
3 files Mathlib.Algebra.Category.Grp.Adjunctions Mathlib.GroupTheory.FreeAbelianGroup Mathlib.RingTheory.FreeRing	-40
Mathlib.GroupTheory.HNNExtension	-36
Mathlib.CategoryTheory.Action.Monoidal	-22
3 files Mathlib.CategoryTheory.Galois.Action Mathlib.CategoryTheory.Galois.Examples Mathlib.CategoryTheory.Galois.Full	-18
18 files Mathlib.Algebra.Algebra.ZMod Mathlib.Algebra.Homology.BifunctorFlip Mathlib.Algebra.Homology.Bifunctor Mathlib.Algebra.Homology.ComplexShapeSigns Mathlib.Algebra.Homology.TotalComplexSymmetry Mathlib.Algebra.Homology.TotalComplex Mathlib.Algebra.Ring.NegOnePow Mathlib.Combinatorics.SimpleGraph.DegreeSum Mathlib.Combinatorics.SimpleGraph.Matching Mathlib.Combinatorics.SimpleGraph.UniversalVerts Mathlib.Data.ZMod.Aut Mathlib.Data.ZMod.Basic Mathlib.Data.ZMod.IntUnitsPower Mathlib.GroupTheory.GroupAction.Blocks Mathlib.GroupTheory.NoncommPiCoprod Mathlib.GroupTheory.OrderOfElement Mathlib.LinearAlgebra.FiniteSpan Mathlib.RingTheory.Fintype	-9
14 files Mathlib.Algebra.Homology.BifunctorAssociator Mathlib.Algebra.Homology.Monoidal Mathlib.CategoryTheory.Localization.Triangulated Mathlib.CategoryTheory.Triangulated.Adjunction Mathlib.CategoryTheory.Triangulated.Functor Mathlib.CategoryTheory.Triangulated.HomologicalFunctor Mathlib.CategoryTheory.Triangulated.Opposite.Functor Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated Mathlib.CategoryTheory.Triangulated.Pretriangulated Mathlib.CategoryTheory.Triangulated.Subcategory Mathlib.CategoryTheory.Triangulated.TStructure.Basic Mathlib.CategoryTheory.Triangulated.TriangleShift Mathlib.CategoryTheory.Triangulated.Triangulated Mathlib.RingTheory.WittVector.WittPolynomial	-8
Mathlib.Data.ZMod.ValMinAbs	-6
21 files Mathlib.Algebra.Homology.BifunctorHomotopy Mathlib.Algebra.Homology.BifunctorShift Mathlib.Algebra.Homology.DerivedCategory.Basic Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass Mathlib.Algebra.Homology.DerivedCategory.HomologySequence Mathlib.Algebra.Homology.DerivedCategory.ShortExact Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift Mathlib.Algebra.Homology.HomotopyCategory.HomComplex Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor Mathlib.Algebra.Homology.HomotopyCategory.MappingCone Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence Mathlib.Algebra.Homology.HomotopyCategory.Shift Mathlib.Algebra.Homology.HomotopyCategory.ShortExact Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors Mathlib.Algebra.Homology.HomotopyCategory.Triangulated Mathlib.Algebra.Homology.TotalComplexShift	-5
4 files Mathlib.GroupTheory.CosetCover Mathlib.GroupTheory.IndexNormal Mathlib.Topology.Algebra.ClopenNhdofOne Mathlib.Topology.Algebra.ClosedSubgroup	-3
435 files Mathlib.Algebra.CharP.CharAndCard Mathlib.Algebra.CharP.Quotient Mathlib.Algebra.CharP.Two Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences Mathlib.Algebra.Order.AbsoluteValue.Equivalence Mathlib.Algebra.Order.Chebyshev Mathlib.Algebra.Order.ToIntervalMod Mathlib.Algebra.Periodic Mathlib.Analysis.Analytic.Basic Mathlib.Analysis.Analytic.CPolynomial Mathlib.Analysis.Analytic.ChangeOrigin Mathlib.Analysis.Analytic.Composition Mathlib.Analysis.Analytic.Constructions Mathlib.Analysis.Analytic.Inverse Mathlib.Analysis.Analytic.IsolatedZeros Mathlib.Analysis.Analytic.IteratedFDeriv Mathlib.Analysis.Analytic.Linear Mathlib.Analysis.Analytic.Meromorphic Mathlib.Analysis.Analytic.OfScalars Mathlib.Analysis.Analytic.RadiusLiminf Mathlib.Analysis.Analytic.Uniqueness Mathlib.Analysis.Analytic.Within Mathlib.Analysis.Asymptotics.AsymptoticEquivalent Mathlib.Analysis.Asymptotics.SpecificAsymptotics Mathlib.Analysis.Asymptotics.SuperpolynomialDecay Mathlib.Analysis.Asymptotics.TVS Mathlib.Analysis.Asymptotics.Theta Mathlib.Analysis.BoxIntegral.Partition.Additive Mathlib.Analysis.CStarAlgebra.Basic Mathlib.Analysis.CStarAlgebra.Classes Mathlib.Analysis.CStarAlgebra.ContinuousMap Mathlib.Analysis.CStarAlgebra.Exponential Mathlib.Analysis.CStarAlgebra.Multiplier Mathlib.Analysis.CStarAlgebra.Unitization Mathlib.Analysis.CStarAlgebra.lpSpace Mathlib.Analysis.Calculus.AddTorsor.AffineMap Mathlib.Analysis.Calculus.Conformal.NormedSpace Mathlib.Analysis.Calculus.ContDiff.Basic Mathlib.Analysis.Calculus.ContDiff.Bounds Mathlib.Analysis.Calculus.ContDiff.CPolynomial Mathlib.Analysis.Calculus.ContDiff.Defs Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno Mathlib.Analysis.Calculus.DSlope Mathlib.Analysis.Calculus.Darboux Mathlib.Analysis.Calculus.Deriv.Add Mathlib.Analysis.Calculus.Deriv.AffineMap Mathlib.Analysis.Calculus.Deriv.Basic Mathlib.Analysis.Calculus.Deriv.Comp Mathlib.Analysis.Calculus.Deriv.Inv Mathlib.Analysis.Calculus.Deriv.Inverse Mathlib.Analysis.Calculus.Deriv.Linear Mathlib.Analysis.Calculus.Deriv.Mul Mathlib.Analysis.Calculus.Deriv.Pi Mathlib.Analysis.Calculus.Deriv.Polynomial Mathlib.Analysis.Calculus.Deriv.Pow Mathlib.Analysis.Calculus.Deriv.Prod Mathlib.Analysis.Calculus.Deriv.Shift Mathlib.Analysis.Calculus.Deriv.Slope Mathlib.Analysis.Calculus.Deriv.Star Mathlib.Analysis.Calculus.Deriv.Support Mathlib.Analysis.Calculus.Deriv.ZPow Mathlib.Analysis.Calculus.DiffContOnCl Mathlib.Analysis.Calculus.FDeriv.Add Mathlib.Analysis.Calculus.FDeriv.Analytic Mathlib.Analysis.Calculus.FDeriv.Basic Mathlib.Analysis.Calculus.FDeriv.Bilinear Mathlib.Analysis.Calculus.FDeriv.Comp Mathlib.Analysis.Calculus.FDeriv.Equiv Mathlib.Analysis.Calculus.FDeriv.Linear Mathlib.Analysis.Calculus.FDeriv.Mul Mathlib.Analysis.Calculus.FDeriv.Pi Mathlib.Analysis.Calculus.FDeriv.Prod Mathlib.Analysis.Calculus.FDeriv.RestrictScalars Mathlib.Analysis.Calculus.FDeriv.Star Mathlib.Analysis.Calculus.FormalMultilinearSeries Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv Mathlib.Analysis.Calculus.IteratedDeriv.Defs Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas Mathlib.Analysis.Calculus.LineDeriv.Basic Mathlib.Analysis.Calculus.LocalExtr.Basic Mathlib.Analysis.Calculus.LocalExtr.LineDeriv Mathlib.Analysis.Calculus.LocalExtr.Rolle Mathlib.Analysis.Calculus.LogDeriv Mathlib.Analysis.Calculus.TangentCone Mathlib.Analysis.Complex.AbelLimit Mathlib.Analysis.Complex.Asymptotics Mathlib.Analysis.Complex.Basic Mathlib.Analysis.Complex.Circle Mathlib.Analysis.Complex.Convex Mathlib.Analysis.Complex.HalfPlane Mathlib.Analysis.Complex.ReImTopology Mathlib.Analysis.Complex.RealDeriv Mathlib.Analysis.Complex.UnitDisc.Basic Mathlib.Analysis.ConstantSpeed Mathlib.Analysis.Convex.Birkhoff Mathlib.Analysis.Convex.Body Mathlib.Analysis.Convex.EGauge Mathlib.Analysis.Convex.Gauge Mathlib.Analysis.Convex.PartitionOfUnity Mathlib.Analysis.Convex.SpecificFunctions.Basic Mathlib.Analysis.Convex.SpecificFunctions.Pow Mathlib.Analysis.InnerProductSpace.Defs Mathlib.Analysis.LocallyConvex.AbsConvex Mathlib.Analysis.LocallyConvex.BalancedCoreHull Mathlib.Analysis.LocallyConvex.Barrelled Mathlib.Analysis.LocallyConvex.Basic Mathlib.Analysis.LocallyConvex.Bounded Mathlib.Analysis.LocallyConvex.ContinuousOfBounded Mathlib.Analysis.LocallyConvex.StrongTopology Mathlib.Analysis.LocallyConvex.WeakDual Mathlib.Analysis.LocallyConvex.WithSeminorms Mathlib.Analysis.MeanInequalitiesPow Mathlib.Analysis.MeanInequalities Mathlib.Analysis.Normed.Affine.AddTorsor Mathlib.Analysis.Normed.Affine.ContinuousAffineMap Mathlib.Analysis.Normed.Affine.Isometry Mathlib.Analysis.Normed.Affine.MazurUlam Mathlib.Analysis.Normed.Algebra.Exponential Mathlib.Analysis.Normed.Algebra.Norm Mathlib.Analysis.Normed.Algebra.Ultra Mathlib.Analysis.Normed.Algebra.Unitization Mathlib.Analysis.Normed.Field.InfiniteSum Mathlib.Analysis.Normed.Field.Lemmas Mathlib.Analysis.Normed.Field.ProperSpace Mathlib.Analysis.Normed.Field.UnitBall Mathlib.Analysis.Normed.Group.AddCircle Mathlib.Analysis.Normed.Group.ControlledClosure Mathlib.Analysis.Normed.Group.Quotient Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels Mathlib.Analysis.Normed.Group.Tannery Mathlib.Analysis.Normed.Group.ZeroAtInfty Mathlib.Analysis.Normed.Lp.lpSpace Mathlib.Analysis.Normed.Module.Basic Mathlib.Analysis.Normed.Module.Completion Mathlib.Analysis.Normed.Module.Ray Mathlib.Analysis.Normed.Module.Span Mathlib.Analysis.Normed.Operator.BanachSteinhaus Mathlib.Analysis.Normed.Operator.Banach Mathlib.Analysis.Normed.Operator.BoundedLinearMaps Mathlib.Analysis.Normed.Operator.Compact Mathlib.Analysis.Normed.Order.Basic Mathlib.Analysis.Normed.Order.UpperLower Mathlib.Analysis.Normed.Ring.IsPowMulFaithful Mathlib.Analysis.Normed.Ring.SeminormFromBounded Mathlib.Analysis.Normed.Ring.SeminormFromConst Mathlib.Analysis.Normed.Ring.Seminorm Mathlib.Analysis.Normed.Ring.Units Mathlib.Analysis.Normed.Ring.WithAbs Mathlib.Analysis.NormedSpace.BallAction Mathlib.Analysis.NormedSpace.ConformalLinearMap Mathlib.Analysis.NormedSpace.ENormedSpace Mathlib.Analysis.NormedSpace.Extend Mathlib.Analysis.NormedSpace.Extr Mathlib.Analysis.NormedSpace.HomeomorphBall Mathlib.Analysis.NormedSpace.Int Mathlib.Analysis.NormedSpace.Multilinear.Basic Mathlib.Analysis.NormedSpace.Multilinear.Curry Mathlib.Analysis.NormedSpace.OperatorNorm.Asymptotics Mathlib.Analysis.NormedSpace.OperatorNorm.Basic Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear Mathlib.Analysis.NormedSpace.OperatorNorm.Completeness Mathlib.Analysis.NormedSpace.OperatorNorm.Mul Mathlib.Analysis.NormedSpace.OperatorNorm.NNNorm Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace Mathlib.Analysis.NormedSpace.OperatorNorm.Prod Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm Mathlib.Analysis.NormedSpace.PiTensorProduct.ProjectiveSeminorm Mathlib.Analysis.NormedSpace.Pointwise Mathlib.Analysis.NormedSpace.RCLike Mathlib.Analysis.NormedSpace.Real Mathlib.Analysis.NormedSpace.RieszLemma Mathlib.Analysis.NormedSpace.SphereNormEquiv Mathlib.Analysis.PSeries Mathlib.Analysis.Polynomial.Basic Mathlib.Analysis.RCLike.Basic Mathlib.Analysis.Seminorm Mathlib.Analysis.SpecialFunctions.CompareExp Mathlib.Analysis.SpecialFunctions.Complex.Arg Mathlib.Analysis.SpecialFunctions.Complex.Circle Mathlib.Analysis.SpecialFunctions.Complex.Log Mathlib.Analysis.SpecialFunctions.Exp Mathlib.Analysis.SpecialFunctions.Exponential Mathlib.Analysis.SpecialFunctions.Log.Base Mathlib.Analysis.SpecialFunctions.Log.Basic Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog Mathlib.Analysis.SpecialFunctions.Log.Monotone Mathlib.Analysis.SpecialFunctions.Log.PosLog Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric Mathlib.Analysis.SpecialFunctions.PolynomialExp Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics Mathlib.Analysis.SpecialFunctions.Pow.Complex Mathlib.Analysis.SpecialFunctions.Pow.Continuity Mathlib.Analysis.SpecialFunctions.Pow.NNReal Mathlib.Analysis.SpecialFunctions.Pow.Real Mathlib.Analysis.SpecialFunctions.Sqrt Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse Mathlib.Analysis.SpecialFunctions.Trigonometric.Series Mathlib.Analysis.SpecificLimits.FloorPow Mathlib.Analysis.SpecificLimits.Normed Mathlib.Analysis.SpecificLimits.RCLike Mathlib.Analysis.SumOverResidueClass Mathlib.CategoryTheory.Abelian.ProjectiveDimension Mathlib.CategoryTheory.Triangulated.Yoneda Mathlib.Combinatorics.Additive.Corner.Roth Mathlib.Combinatorics.Derangements.Exponential Mathlib.Combinatorics.SimpleGraph.Regularity.Bound Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk Mathlib.Combinatorics.SimpleGraph.Regularity.Increment Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma Mathlib.Combinatorics.SimpleGraph.Triangle.Removal Mathlib.Computability.AkraBazzi.GrowsPolynomially Mathlib.Condensed.AB Mathlib.Condensed.Basic Mathlib.Condensed.CartesianClosed Mathlib.Condensed.Discrete.Basic Mathlib.Condensed.Discrete.Characterization Mathlib.Condensed.Discrete.Colimit Mathlib.Condensed.Discrete.LocallyConstant Mathlib.Condensed.Discrete.Module Mathlib.Condensed.Epi Mathlib.Condensed.Equivalence Mathlib.Condensed.Explicit Mathlib.Condensed.Functors Mathlib.Condensed.Light.AB Mathlib.Condensed.Light.Basic Mathlib.Condensed.Light.CartesianClosed Mathlib.Condensed.Light.Epi Mathlib.Condensed.Light.Explicit Mathlib.Condensed.Light.Functors Mathlib.Condensed.Light.Limits Mathlib.Condensed.Light.Module Mathlib.Condensed.Light.TopCatAdjunction Mathlib.Condensed.Light.TopComparison Mathlib.Condensed.Limits Mathlib.Condensed.Module Mathlib.Condensed.Solid Mathlib.Condensed.TopCatAdjunction Mathlib.Condensed.TopComparison Mathlib.Data.Matrix.DoublyStochastic Mathlib.Data.Nat.Periodic Mathlib.Data.Nat.Totient Mathlib.Data.ZMod.Factorial Mathlib.Data.ZMod.Units Mathlib.Dynamics.BirkhoffSum.NormedSpace Mathlib.Dynamics.Ergodic.Action.Regular Mathlib.Dynamics.Ergodic.Function Mathlib.Dynamics.TopologicalEntropy.CoverEntropy Mathlib.Dynamics.TopologicalEntropy.NetEntropy Mathlib.Dynamics.TopologicalEntropy.Semiconj Mathlib.Geometry.Manifold.ConformalGroupoid Mathlib.GroupTheory.Coxeter.Inversion Mathlib.GroupTheory.Coxeter.Length Mathlib.GroupTheory.Exponent Mathlib.GroupTheory.FixedPointFree Mathlib.GroupTheory.GroupAction.Period Mathlib.GroupTheory.Perm.Closure Mathlib.GroupTheory.Perm.ConjAct Mathlib.GroupTheory.Perm.Cycle.Basic Mathlib.GroupTheory.Perm.Cycle.Concrete Mathlib.GroupTheory.Perm.Cycle.Factors Mathlib.GroupTheory.Perm.Cycle.PossibleTypes Mathlib.GroupTheory.Perm.Cycle.Type Mathlib.GroupTheory.Perm.Fin Mathlib.GroupTheory.Perm.Finite Mathlib.GroupTheory.SpecificGroups.Alternating Mathlib.GroupTheory.SpecificGroups.Dihedral Mathlib.LinearAlgebra.CrossProduct Mathlib.LinearAlgebra.Matrix.AbsoluteValue Mathlib.LinearAlgebra.Matrix.Basis Mathlib.LinearAlgebra.Matrix.Determinant.Basic Mathlib.LinearAlgebra.Matrix.Determinant.Misc Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular Mathlib.LinearAlgebra.Matrix.MvPolynomial Mathlib.LinearAlgebra.Matrix.Permutation Mathlib.LinearAlgebra.Matrix.Polynomial Mathlib.LinearAlgebra.Matrix.Reindex Mathlib.LinearAlgebra.Matrix.Transvection Mathlib.LinearAlgebra.TensorProduct.Graded.External Mathlib.LinearAlgebra.TensorProduct.Graded.Internal Mathlib.MeasureTheory.Category.MeasCat Mathlib.MeasureTheory.Constructions.BorelSpace.Complex Mathlib.MeasureTheory.Constructions.BorelSpace.Metric Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable Mathlib.MeasureTheory.Constructions.BorelSpace.Real Mathlib.MeasureTheory.Constructions.Pi Mathlib.MeasureTheory.Constructions.Polish.Basic Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal Mathlib.MeasureTheory.Function.AEEqFun Mathlib.MeasureTheory.Function.AEEqOfLIntegral Mathlib.MeasureTheory.Function.ConvergenceInMeasure Mathlib.MeasureTheory.Function.Egorov Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral Mathlib.MeasureTheory.Function.LpOrder Mathlib.MeasureTheory.Function.LpSeminorm.Basic Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality Mathlib.MeasureTheory.Function.LpSeminorm.Trim Mathlib.MeasureTheory.Function.LpSpace Mathlib.MeasureTheory.Function.SimpleFuncDense Mathlib.MeasureTheory.Function.SpecialFunctions.Arctan Mathlib.MeasureTheory.Function.SpecialFunctions.Basic Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic Mathlib.MeasureTheory.Function.StronglyMeasurable.ENNReal Mathlib.MeasureTheory.Group.Convolution Mathlib.MeasureTheory.Group.LIntegral Mathlib.MeasureTheory.Group.Measure Mathlib.MeasureTheory.Group.Prod Mathlib.MeasureTheory.Integral.Indicator Mathlib.MeasureTheory.Integral.LebesgueNormedSpace Mathlib.MeasureTheory.Integral.Lebesgue Mathlib.MeasureTheory.Integral.Marginal Mathlib.MeasureTheory.Integral.MeanInequalities Mathlib.MeasureTheory.Integral.RieszMarkovKakutani Mathlib.MeasureTheory.Measure.Complex Mathlib.MeasureTheory.Measure.Doubling Mathlib.MeasureTheory.Measure.EverywherePos Mathlib.MeasureTheory.Measure.GiryMonad Mathlib.MeasureTheory.Measure.Haar.Basic Mathlib.MeasureTheory.Measure.HasOuterApproxClosed Mathlib.MeasureTheory.Measure.Prod Mathlib.MeasureTheory.Measure.WithDensity Mathlib.NumberTheory.DirichletCharacter.Basic Mathlib.NumberTheory.EulerProduct.Basic Mathlib.NumberTheory.Harmonic.Int Mathlib.NumberTheory.LegendreSymbol.ZModChar Mathlib.NumberTheory.LucasLehmer Mathlib.NumberTheory.MulChar.Basic Mathlib.NumberTheory.Ostrowski Mathlib.NumberTheory.Padics.PadicNumbers Mathlib.NumberTheory.PrimeCounting Mathlib.NumberTheory.SumPrimeReciprocals Mathlib.NumberTheory.VonMangoldt Mathlib.Probability.Distributions.Geometric Mathlib.Probability.Distributions.Poisson Mathlib.Probability.Independence.Basic Mathlib.Probability.Independence.Kernel Mathlib.Probability.Kernel.Basic Mathlib.Probability.Kernel.Composition.Basic Mathlib.Probability.Kernel.Composition.CompNotation Mathlib.Probability.Kernel.Composition.ParallelComp Mathlib.Probability.Kernel.Defs Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes Mathlib.Probability.Kernel.Invariance Mathlib.Probability.Kernel.MeasurableLIntegral Mathlib.Probability.Kernel.Proper Mathlib.RingTheory.Binomial Mathlib.RingTheory.Polynomial.Chebyshev Mathlib.RingTheory.Polynomial.Dickson Mathlib.RingTheory.PowerSeries.Binomial Mathlib.SetTheory.Nimber.Field Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits Mathlib.Topology.Algebra.Module.Alternating.Topology Mathlib.Topology.Algebra.Module.Cardinality Mathlib.Topology.Algebra.Module.Multilinear.Bounded Mathlib.Topology.Algebra.Module.Multilinear.Topology Mathlib.Topology.Algebra.Module.StrongTopology Mathlib.Topology.Algebra.Module.UniformConvergence Mathlib.Topology.Algebra.PontryaginDual Mathlib.Topology.Algebra.ProperAction.ProperlyDiscontinuous Mathlib.Topology.Bornology.BoundedOperation Mathlib.Topology.Category.CompHaus.Basic Mathlib.Topology.Category.CompHaus.EffectiveEpi Mathlib.Topology.Category.CompHaus.Frm Mathlib.Topology.Category.CompHaus.Limits Mathlib.Topology.Category.CompHaus.Projective Mathlib.Topology.Category.CompactlyGenerated Mathlib.Topology.Category.Compactum Mathlib.Topology.Category.DeltaGenerated Mathlib.Topology.Category.LightProfinite.AsLimit Mathlib.Topology.Category.LightProfinite.Basic Mathlib.Topology.Category.LightProfinite.EffectiveEpi Mathlib.Topology.Category.LightProfinite.Extend Mathlib.Topology.Category.LightProfinite.Limits Mathlib.Topology.Category.LightProfinite.Sequence Mathlib.Topology.Category.Locale Mathlib.Topology.Category.Profinite.AsLimit Mathlib.Topology.Category.Profinite.Basic Mathlib.Topology.Category.Profinite.CofilteredLimit Mathlib.Topology.Category.Profinite.EffectiveEpi Mathlib.Topology.Category.Profinite.Extend Mathlib.Topology.Category.Profinite.Limits Mathlib.Topology.Category.Profinite.Product Mathlib.Topology.Category.Profinite.Projective Mathlib.Topology.Category.Stonean.Adjunctions Mathlib.Topology.Category.Stonean.Basic Mathlib.Topology.Category.Stonean.EffectiveEpi Mathlib.Topology.Category.Stonean.Limits Mathlib.Topology.Compactness.CompactlyGeneratedSpace Mathlib.Topology.Compactness.DeltaGeneratedSpace Mathlib.Topology.ContinuousMap.Bounded.Basic Mathlib.Topology.ContinuousMap.Bounded.Star Mathlib.Topology.ContinuousMap.BoundedCompactlySupported Mathlib.Topology.ContinuousMap.Compact Mathlib.Topology.ContinuousMap.CompactlySupported Mathlib.Topology.ContinuousMap.ContinuousMapZero Mathlib.Topology.ContinuousMap.Ideals Mathlib.Topology.ContinuousMap.Periodic Mathlib.Topology.ContinuousMap.StarOrdered Mathlib.Topology.ContinuousMap.Units Mathlib.Topology.ContinuousMap.ZeroAtInfty Mathlib.Topology.Germ Mathlib.Topology.Instances.AddCircle Mathlib.Topology.Instances.Real.Lemmas Mathlib.Topology.Maps.Proper.CompactlyGenerated Mathlib.Topology.MetricSpace.GromovHausdorffRealized Mathlib.Topology.MetricSpace.GromovHausdorff Mathlib.Topology.MetricSpace.HolderNorm Mathlib.Topology.MetricSpace.Holder Mathlib.Topology.MetricSpace.Kuratowski Mathlib.Topology.MetricSpace.PartitionOfUnity Mathlib.Topology.MetricSpace.ThickenedIndicator Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps Mathlib.Topology.Metrizable.Urysohn Mathlib.Topology.Order.Category.FrameAdjunction Mathlib.Topology.PartitionOfUnity Mathlib.Topology.Separation.CompletelyRegular Mathlib.Topology.Separation.NotNormal Mathlib.Topology.TietzeExtension Mathlib.Topology.UrysohnsBounded Mathlib.Topology.UrysohnsLemma Mathlib.Topology.VectorBundle.Basic Mathlib.Topology.VectorBundle.Constructions Mathlib.Topology.VectorBundle.Hom	-2
916 files Mathlib.Algebra.BrauerGroup.Defs Mathlib.Algebra.Category.Grp.EnoughInjectives Mathlib.Algebra.Category.Grp.Injective Mathlib.Algebra.Category.Grp.LargeColimits Mathlib.Algebra.Category.Grp.Ulift Mathlib.Algebra.Category.ModuleCat.EnoughInjectives Mathlib.Algebra.Category.Ring.LinearAlgebra Mathlib.Algebra.Category.Ring.Under.Limits Mathlib.Algebra.Central.TensorProduct Mathlib.Algebra.Colimit.Ring Mathlib.Algebra.DirectSum.LinearMap Mathlib.Algebra.FreeAlgebra.Cardinality Mathlib.Algebra.GCDMonoid.IntegrallyClosed Mathlib.Algebra.Lie.CartanExists Mathlib.Algebra.Lie.CartanSubalgebra Mathlib.Algebra.Lie.Character Mathlib.Algebra.Lie.Derivation.Killing Mathlib.Algebra.Lie.EngelSubalgebra Mathlib.Algebra.Lie.Engel Mathlib.Algebra.Lie.InvariantForm Mathlib.Algebra.Lie.Killing Mathlib.Algebra.Lie.LieTheorem Mathlib.Algebra.Lie.Nilpotent Mathlib.Algebra.Lie.Rank Mathlib.Algebra.Lie.Semisimple.Basic Mathlib.Algebra.Lie.Semisimple.Defs Mathlib.Algebra.Lie.Solvable Mathlib.Algebra.Lie.TraceForm Mathlib.Algebra.Lie.Weights.Basic Mathlib.Algebra.Lie.Weights.Cartan Mathlib.Algebra.Lie.Weights.Chain Mathlib.Algebra.Lie.Weights.Linear Mathlib.Algebra.Module.CharacterModule Mathlib.Algebra.Module.LinearMap.Polynomial Mathlib.Algebra.Module.ZLattice.Basic Mathlib.Algebra.Module.ZLattice.Covolume Mathlib.Algebra.Polynomial.Bivariate Mathlib.Algebra.Polynomial.GroupRingAction Mathlib.AlgebraicGeometry.AffineScheme Mathlib.AlgebraicGeometry.AffineSpace Mathlib.AlgebraicGeometry.Cover.MorphismProperty Mathlib.AlgebraicGeometry.Cover.Open Mathlib.AlgebraicGeometry.Cover.Over Mathlib.AlgebraicGeometry.EllipticCurve.Affine Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree Mathlib.AlgebraicGeometry.EllipticCurve.Group Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian Mathlib.AlgebraicGeometry.EllipticCurve.Projective Mathlib.AlgebraicGeometry.Fiber Mathlib.AlgebraicGeometry.FunctionField Mathlib.AlgebraicGeometry.GammaSpecAdjunction Mathlib.AlgebraicGeometry.GluingOneHypercover Mathlib.AlgebraicGeometry.Gluing Mathlib.AlgebraicGeometry.Limits Mathlib.AlgebraicGeometry.Modules.Presheaf Mathlib.AlgebraicGeometry.Modules.Sheaf Mathlib.AlgebraicGeometry.Modules.Tilde Mathlib.AlgebraicGeometry.Morphisms.AffineAnd Mathlib.AlgebraicGeometry.Morphisms.Affine Mathlib.AlgebraicGeometry.Morphisms.Basic Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion Mathlib.AlgebraicGeometry.Morphisms.Constructors Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation Mathlib.AlgebraicGeometry.Morphisms.FiniteType Mathlib.AlgebraicGeometry.Morphisms.Finite Mathlib.AlgebraicGeometry.Morphisms.Flat Mathlib.AlgebraicGeometry.Morphisms.Immersion Mathlib.AlgebraicGeometry.Morphisms.Integral Mathlib.AlgebraicGeometry.Morphisms.IsIso Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion Mathlib.AlgebraicGeometry.Morphisms.Preimmersion Mathlib.AlgebraicGeometry.Morphisms.Proper Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties Mathlib.AlgebraicGeometry.Morphisms.Separated Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective Mathlib.AlgebraicGeometry.Noetherian Mathlib.AlgebraicGeometry.OpenImmersion Mathlib.AlgebraicGeometry.Over Mathlib.AlgebraicGeometry.PointsPi Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme Mathlib.AlgebraicGeometry.Properties Mathlib.AlgebraicGeometry.PullbackCarrier Mathlib.AlgebraicGeometry.Pullbacks Mathlib.AlgebraicGeometry.RationalMap Mathlib.AlgebraicGeometry.ResidueField Mathlib.AlgebraicGeometry.Restrict Mathlib.AlgebraicGeometry.Scheme Mathlib.AlgebraicGeometry.Sites.BigZariski Mathlib.AlgebraicGeometry.Sites.MorphismProperty Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski Mathlib.AlgebraicGeometry.Sites.Small Mathlib.AlgebraicGeometry.Spec Mathlib.AlgebraicGeometry.SpreadingOut Mathlib.AlgebraicGeometry.Stalk Mathlib.AlgebraicGeometry.StructureSheaf Mathlib.AlgebraicGeometry.ValuativeCriterion Mathlib.Analysis.Analytic.Polynomial Mathlib.Analysis.Asymptotics.Lemmas Mathlib.Analysis.BoundedVariation Mathlib.Analysis.BoxIntegral.Basic Mathlib.Analysis.BoxIntegral.Box.SubboxInduction Mathlib.Analysis.BoxIntegral.DivergenceTheorem Mathlib.Analysis.BoxIntegral.Integrability Mathlib.Analysis.BoxIntegral.Partition.Filter Mathlib.Analysis.BoxIntegral.Partition.Measure Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction Mathlib.Analysis.BoxIntegral.UnitPartition Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap Mathlib.Analysis.CStarAlgebra.Matrix Mathlib.Analysis.CStarAlgebra.Module.Synonym Mathlib.Analysis.Calculus.AddTorsor.Coord Mathlib.Analysis.Calculus.BumpFunction.Basic Mathlib.Analysis.Calculus.BumpFunction.Convolution Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension Mathlib.Analysis.Calculus.BumpFunction.InnerProduct Mathlib.Analysis.Calculus.BumpFunction.Normed Mathlib.Analysis.Calculus.Conformal.InnerProduct Mathlib.Analysis.Calculus.ContDiff.FiniteDimension Mathlib.Analysis.Calculus.ContDiff.RCLike Mathlib.Analysis.Calculus.ContDiff.WithLp Mathlib.Analysis.Calculus.Deriv.Abs Mathlib.Analysis.Calculus.FDeriv.Extend Mathlib.Analysis.Calculus.FDeriv.Measurable Mathlib.Analysis.Calculus.FDeriv.Norm Mathlib.Analysis.Calculus.FDeriv.Symmetric Mathlib.Analysis.Calculus.FDeriv.WithLp Mathlib.Analysis.Calculus.FirstDerivativeTest Mathlib.Analysis.Calculus.Gradient.Basic Mathlib.Analysis.Calculus.Implicit Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional Mathlib.Analysis.Calculus.LHopital Mathlib.Analysis.Calculus.LagrangeMultipliers Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts Mathlib.Analysis.Calculus.LineDeriv.Measurable Mathlib.Analysis.Calculus.LocalExtr.Polynomial Mathlib.Analysis.Calculus.MeanValue Mathlib.Analysis.Calculus.Monotone Mathlib.Analysis.Calculus.ParametricIntegral Mathlib.Analysis.Calculus.ParametricIntervalIntegral Mathlib.Analysis.Calculus.Rademacher Mathlib.Analysis.Calculus.SmoothSeries Mathlib.Analysis.Calculus.Taylor Mathlib.Analysis.Calculus.UniformLimitsDeriv Mathlib.Analysis.Calculus.VectorField Mathlib.Analysis.Complex.AbsMax Mathlib.Analysis.Complex.Angle Mathlib.Analysis.Complex.Arg Mathlib.Analysis.Complex.CauchyIntegral Mathlib.Analysis.Complex.Hadamard Mathlib.Analysis.Complex.IsIntegral Mathlib.Analysis.Complex.Liouville Mathlib.Analysis.Complex.LocallyUniformLimit Mathlib.Analysis.Complex.OpenMapping Mathlib.Analysis.Complex.OperatorNorm Mathlib.Analysis.Complex.Periodic Mathlib.Analysis.Complex.PhragmenLindelof Mathlib.Analysis.Complex.Positivity Mathlib.Analysis.Complex.RemovableSingularity Mathlib.Analysis.Complex.Schwarz Mathlib.Analysis.Complex.TaylorSeries Mathlib.Analysis.Complex.Tietze Mathlib.Analysis.Convex.AmpleSet Mathlib.Analysis.Convex.Cone.Closure Mathlib.Analysis.Convex.Cone.InnerDual Mathlib.Analysis.Convex.Cone.Pointed Mathlib.Analysis.Convex.Cone.Proper Mathlib.Analysis.Convex.Continuous Mathlib.Analysis.Convex.Deriv Mathlib.Analysis.Convex.Exposed Mathlib.Analysis.Convex.GaugeRescale Mathlib.Analysis.Convex.Integral Mathlib.Analysis.Convex.Intrinsic Mathlib.Analysis.Convex.KreinMilman Mathlib.Analysis.Convex.Measure Mathlib.Analysis.Convex.Normed Mathlib.Analysis.Convex.Side Mathlib.Analysis.Convex.SpecificFunctions.Deriv Mathlib.Analysis.Convex.StrictConvexBetween Mathlib.Analysis.Convex.StrictConvexSpace Mathlib.Analysis.Convex.Strong Mathlib.Analysis.Convex.Topology Mathlib.Analysis.Convex.TotallyBounded Mathlib.Analysis.Convex.Uniform Mathlib.Analysis.Convolution Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff Mathlib.Analysis.Distribution.FourierSchwartz Mathlib.Analysis.Distribution.SchwartzSpace Mathlib.Analysis.Fourier.AddCircleMulti Mathlib.Analysis.Fourier.AddCircle Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality Mathlib.Analysis.Fourier.FourierTransformDeriv Mathlib.Analysis.Fourier.FourierTransform Mathlib.Analysis.Fourier.Inversion Mathlib.Analysis.Fourier.PoissonSummation Mathlib.Analysis.Fourier.RiemannLebesgueLemma Mathlib.Analysis.FunctionalSpaces.SobolevInequality Mathlib.Analysis.Hofer Mathlib.Analysis.InnerProductSpace.Adjoint Mathlib.Analysis.InnerProductSpace.Basic Mathlib.Analysis.InnerProductSpace.Calculus Mathlib.Analysis.InnerProductSpace.Completion Mathlib.Analysis.InnerProductSpace.ConformalLinearMap Mathlib.Analysis.InnerProductSpace.Dual Mathlib.Analysis.InnerProductSpace.EuclideanDist Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho Mathlib.Analysis.InnerProductSpace.LaxMilgram Mathlib.Analysis.InnerProductSpace.LinearMap Mathlib.Analysis.InnerProductSpace.LinearPMap Mathlib.Analysis.InnerProductSpace.MeanErgodic Mathlib.Analysis.InnerProductSpace.NormPow Mathlib.Analysis.InnerProductSpace.OfNorm Mathlib.Analysis.InnerProductSpace.Orientation Mathlib.Analysis.InnerProductSpace.Orthogonal Mathlib.Analysis.InnerProductSpace.Orthonormal Mathlib.Analysis.InnerProductSpace.PiL2 Mathlib.Analysis.InnerProductSpace.Positive Mathlib.Analysis.InnerProductSpace.ProdL2 Mathlib.Analysis.InnerProductSpace.Projection Mathlib.Analysis.InnerProductSpace.Rayleigh Mathlib.Analysis.InnerProductSpace.Spectrum Mathlib.Analysis.InnerProductSpace.Subspace Mathlib.Analysis.InnerProductSpace.Symmetric Mathlib.Analysis.InnerProductSpace.TwoDim Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology Mathlib.Analysis.InnerProductSpace.l2Space Mathlib.Analysis.LocallyConvex.WeakOperatorTopology Mathlib.Analysis.LocallyConvex.WeakSpace Mathlib.Analysis.Matrix Mathlib.Analysis.MellinInversion Mathlib.Analysis.MellinTransform Mathlib.Analysis.Normed.Affine.AddTorsorBases Mathlib.Analysis.Normed.Algebra.MatrixExponential Mathlib.Analysis.Normed.Algebra.QuaternionExponential Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt Mathlib.Analysis.Normed.Algebra.UnitizationL1 Mathlib.Analysis.Normed.Field.Ultra Mathlib.Analysis.Normed.Group.BallSphere Mathlib.Analysis.Normed.Group.Completeness Mathlib.Analysis.Normed.Group.Completion Mathlib.Analysis.Normed.Group.HomCompletion Mathlib.Analysis.Normed.Group.Hom Mathlib.Analysis.Normed.Group.InfiniteSum Mathlib.Analysis.Normed.Group.Lemmas Mathlib.Analysis.Normed.Group.NullSubmodule Mathlib.Analysis.Normed.Group.Pointwise Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion Mathlib.Analysis.Normed.Group.SemiNormedGrp Mathlib.Analysis.Normed.Group.Ultra Mathlib.Analysis.Normed.Group.Uniform Mathlib.Analysis.Normed.Lp.LpEquiv Mathlib.Analysis.Normed.Lp.PiLp Mathlib.Analysis.Normed.Lp.ProdLp Mathlib.Analysis.Normed.Module.Complemented Mathlib.Analysis.Normed.Module.Dual Mathlib.Analysis.Normed.Module.FiniteDimension Mathlib.Analysis.Normed.Module.WeakDual Mathlib.Analysis.Normed.MulAction Mathlib.Analysis.Normed.Operator.ContinuousLinearMap Mathlib.Analysis.Normed.Operator.LinearIsometry Mathlib.Analysis.Normed.Order.Lattice Mathlib.Analysis.Normed.Ring.Ultra Mathlib.Analysis.NormedSpace.Connected Mathlib.Analysis.NormedSpace.DualNumber Mathlib.Analysis.NormedSpace.FunctionSeries Mathlib.Analysis.NormedSpace.HahnBanach.Extension Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual Mathlib.Analysis.NormedSpace.HahnBanach.Separation Mathlib.Analysis.ODE.Gronwall Mathlib.Analysis.ODE.PicardLindelof Mathlib.Analysis.PSeriesComplex Mathlib.Analysis.Quaternion Mathlib.Analysis.RCLike.Inner Mathlib.Analysis.RCLike.Lemmas Mathlib.Analysis.SpecialFunctions.Arsinh Mathlib.Analysis.SpecialFunctions.Bernstein Mathlib.Analysis.SpecialFunctions.BinaryEntropy Mathlib.Analysis.SpecialFunctions.Complex.Analytic Mathlib.Analysis.SpecialFunctions.Complex.Arctan Mathlib.Analysis.SpecialFunctions.Complex.LogBounds Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic Mathlib.Analysis.SpecialFunctions.ExpDeriv Mathlib.Analysis.SpecialFunctions.Gamma.Basic Mathlib.Analysis.SpecialFunctions.Gamma.Beta Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup Mathlib.Analysis.SpecialFunctions.Gamma.Deligne Mathlib.Analysis.SpecialFunctions.Gamma.Deriv Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation Mathlib.Analysis.SpecialFunctions.ImproperIntegrals Mathlib.Analysis.SpecialFunctions.Integrals Mathlib.Analysis.SpecialFunctions.JapaneseBracket Mathlib.Analysis.SpecialFunctions.Log.Deriv Mathlib.Analysis.SpecialFunctions.Log.NegMulLog Mathlib.Analysis.SpecialFunctions.Log.Summable Mathlib.Analysis.SpecialFunctions.NonIntegrable Mathlib.Analysis.SpecialFunctions.PolarCoord Mathlib.Analysis.SpecialFunctions.Pow.Deriv Mathlib.Analysis.SpecialFunctions.Pow.Integral Mathlib.Analysis.SpecialFunctions.SmoothTransition Mathlib.Analysis.SpecialFunctions.Stirling Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv Mathlib.Analysis.SpecificLimits.Basic Mathlib.Analysis.SumIntegralComparisons Mathlib.Analysis.VonNeumannAlgebra.Basic Mathlib.CategoryTheory.Galois.EssSurj Mathlib.CategoryTheory.Galois.IsFundamentalgroup Mathlib.CategoryTheory.Preadditive.Schur Mathlib.CategoryTheory.Sites.MayerVietorisSquare Mathlib.CategoryTheory.Sites.SheafCohomology.Basic Mathlib.Combinatorics.Additive.AP.Three.Behrend Mathlib.Combinatorics.Additive.Randomisation Mathlib.Combinatorics.Configuration Mathlib.Combinatorics.Extremal.RuzsaSzemeredi Mathlib.Computability.AkraBazzi.AkraBazzi Mathlib.Data.Complex.Cardinality Mathlib.Data.Complex.Determinant Mathlib.Data.Complex.ExponentialBounds Mathlib.Data.Complex.FiniteDimensional Mathlib.Data.Complex.Orientation Mathlib.Data.Matrix.Kronecker Mathlib.Data.Matrix.Rank Mathlib.Data.Nat.Choose.Lucas Mathlib.Data.Nat.Factorial.SuperFactorial Mathlib.Data.Real.Cardinality Mathlib.Data.Real.Hyperreal Mathlib.Data.Real.IsNonarchimedean Mathlib.Data.Real.Pi.Bounds Mathlib.Data.Real.Pi.Irrational Mathlib.Data.Real.Pi.Leibniz Mathlib.Data.Real.Pi.Wallis Mathlib.Data.ZMod.Coprime Mathlib.Data.ZMod.QuotientGroup Mathlib.Data.ZMod.QuotientRing Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber Mathlib.Dynamics.Ergodic.Action.Basic Mathlib.Dynamics.Ergodic.Action.OfMinimal Mathlib.Dynamics.Ergodic.AddCircle Mathlib.Dynamics.Ergodic.Conservative Mathlib.Dynamics.Ergodic.Ergodic Mathlib.Dynamics.Ergodic.MeasurePreserving Mathlib.FieldTheory.AlgebraicClosure Mathlib.FieldTheory.AxGrothendieck Mathlib.FieldTheory.Extension Mathlib.FieldTheory.Fixed Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra Mathlib.FieldTheory.IntermediateField.Adjoin.Basic Mathlib.FieldTheory.IntermediateField.Algebraic Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure Mathlib.FieldTheory.IsAlgClosed.Basic Mathlib.FieldTheory.IsAlgClosed.Classification Mathlib.FieldTheory.IsAlgClosed.Spectrum Mathlib.FieldTheory.KummerPolynomial Mathlib.FieldTheory.Laurent Mathlib.FieldTheory.LinearDisjoint Mathlib.FieldTheory.Minpoly.Field Mathlib.FieldTheory.Minpoly.IsConjRoot Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed Mathlib.FieldTheory.Normal.Basic Mathlib.FieldTheory.Normal.Closure Mathlib.FieldTheory.Normal.Defs Mathlib.FieldTheory.PerfectClosure Mathlib.FieldTheory.Perfect Mathlib.FieldTheory.RatFunc.AsPolynomial Mathlib.FieldTheory.RatFunc.Degree Mathlib.FieldTheory.Relrank Mathlib.FieldTheory.SeparableDegree Mathlib.FieldTheory.Separable Mathlib.FieldTheory.SplittingField.Construction Mathlib.FieldTheory.SplittingField.IsSplittingField Mathlib.Geometry.Euclidean.Angle.Oriented.Affine Mathlib.Geometry.Euclidean.Angle.Oriented.Basic Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation Mathlib.Geometry.Euclidean.Angle.Sphere Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic Mathlib.Geometry.Euclidean.Angle.Unoriented.Conformal Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle Mathlib.Geometry.Euclidean.Basic Mathlib.Geometry.Euclidean.Circumcenter Mathlib.Geometry.Euclidean.Inversion.Basic Mathlib.Geometry.Euclidean.Inversion.Calculus Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane Mathlib.Geometry.Euclidean.MongePoint Mathlib.Geometry.Euclidean.PerpBisector Mathlib.Geometry.Euclidean.Sphere.Basic Mathlib.Geometry.Euclidean.Sphere.Power Mathlib.Geometry.Euclidean.Sphere.Ptolemy Mathlib.Geometry.Euclidean.Sphere.SecondInter Mathlib.Geometry.Euclidean.Triangle Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation Mathlib.Geometry.Manifold.Algebra.LieGroup Mathlib.Geometry.Manifold.Algebra.Monoid Mathlib.Geometry.Manifold.Algebra.SmoothFunctions Mathlib.Geometry.Manifold.Algebra.Structures Mathlib.Geometry.Manifold.AnalyticManifold Mathlib.Geometry.Manifold.BumpFunction Mathlib.Geometry.Manifold.Complex Mathlib.Geometry.Manifold.ContMDiff.Atlas Mathlib.Geometry.Manifold.ContMDiff.Basic Mathlib.Geometry.Manifold.ContMDiff.Defs Mathlib.Geometry.Manifold.ContMDiff.NormedSpace Mathlib.Geometry.Manifold.ContMDiff.Product Mathlib.Geometry.Manifold.ContMDiffMFDeriv Mathlib.Geometry.Manifold.ContMDiffMap Mathlib.Geometry.Manifold.DerivationBundle Mathlib.Geometry.Manifold.Diffeomorph Mathlib.Geometry.Manifold.Instances.Real Mathlib.Geometry.Manifold.Instances.Sphere Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra Mathlib.Geometry.Manifold.IntegralCurve.Basic Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique Mathlib.Geometry.Manifold.IntegralCurve.Transform Mathlib.Geometry.Manifold.IntegralCurve.UniformTime Mathlib.Geometry.Manifold.IsManifold.Basic Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary Mathlib.Geometry.Manifold.LocalDiffeomorph Mathlib.Geometry.Manifold.MFDeriv.Atlas Mathlib.Geometry.Manifold.MFDeriv.Basic Mathlib.Geometry.Manifold.MFDeriv.Defs Mathlib.Geometry.Manifold.MFDeriv.FDeriv Mathlib.Geometry.Manifold.MFDeriv.NormedSpace Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions Mathlib.Geometry.Manifold.MFDeriv.Tangent Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential Mathlib.Geometry.Manifold.Metrizable Mathlib.Geometry.Manifold.PartitionOfUnity Mathlib.Geometry.Manifold.PoincareConjecture Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace Mathlib.Geometry.Manifold.Sheaf.Smooth Mathlib.Geometry.Manifold.VectorBundle.Basic Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear Mathlib.Geometry.Manifold.VectorBundle.Hom Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable Mathlib.Geometry.Manifold.VectorBundle.Pullback Mathlib.Geometry.Manifold.VectorBundle.SmoothSection Mathlib.Geometry.Manifold.VectorBundle.Tangent Mathlib.Geometry.Manifold.VectorField Mathlib.Geometry.Manifold.WhitneyEmbedding Mathlib.GroupTheory.CommutingProbability Mathlib.GroupTheory.FreeAbelianGroupFinsupp Mathlib.GroupTheory.Perm.Centralizer Mathlib.LinearAlgebra.AffineSpace.ContinuousAffineEquiv Mathlib.LinearAlgebra.AffineSpace.Matrix Mathlib.LinearAlgebra.Alternating.DomCoprod Mathlib.LinearAlgebra.AnnihilatingPolynomial Mathlib.LinearAlgebra.Charpoly.BaseChange Mathlib.LinearAlgebra.Charpoly.Basic Mathlib.LinearAlgebra.Charpoly.ToMatrix Mathlib.LinearAlgebra.Determinant Mathlib.LinearAlgebra.Eigenspace.Minpoly Mathlib.LinearAlgebra.Eigenspace.Pi Mathlib.LinearAlgebra.Eigenspace.Triangularizable Mathlib.LinearAlgebra.Eigenspace.Zero Mathlib.LinearAlgebra.FreeModule.Determinant Mathlib.LinearAlgebra.FreeModule.IdealQuotient Mathlib.LinearAlgebra.FreeModule.Int Mathlib.LinearAlgebra.FreeModule.Norm Mathlib.LinearAlgebra.Lagrange Mathlib.LinearAlgebra.LinearDisjoint Mathlib.LinearAlgebra.Matrix.Adjugate Mathlib.LinearAlgebra.Matrix.BaseChange Mathlib.LinearAlgebra.Matrix.Block Mathlib.LinearAlgebra.Matrix.Charpoly.Basic Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly Mathlib.LinearAlgebra.Matrix.Charpoly.Univ Mathlib.LinearAlgebra.Matrix.Gershgorin Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus Mathlib.LinearAlgebra.Matrix.Hermitian Mathlib.LinearAlgebra.Matrix.IsDiag Mathlib.LinearAlgebra.Matrix.Nondegenerate Mathlib.LinearAlgebra.Matrix.NonsingularInverse Mathlib.LinearAlgebra.Matrix.Spectrum Mathlib.LinearAlgebra.Matrix.ZPow Mathlib.LinearAlgebra.Orientation Mathlib.LinearAlgebra.PID Mathlib.LinearAlgebra.PerfectPairing.Restrict Mathlib.LinearAlgebra.Projectivization.Cardinality Mathlib.LinearAlgebra.Projectivization.Constructions Mathlib.LinearAlgebra.SymplecticGroup Mathlib.LinearAlgebra.TensorProduct.Matrix Mathlib.LinearAlgebra.Trace Mathlib.LinearAlgebra.UnitaryGroup Mathlib.LinearAlgebra.Vandermonde Mathlib.MeasureTheory.Constructions.BorelSpace.Basic Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap Mathlib.MeasureTheory.Constructions.BorelSpace.Order Mathlib.MeasureTheory.Constructions.HaarToSphere Mathlib.MeasureTheory.Constructions.Projective Mathlib.MeasureTheory.Constructions.UnitInterval Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace Mathlib.MeasureTheory.Covering.Besicovitch Mathlib.MeasureTheory.Covering.DensityTheorem Mathlib.MeasureTheory.Covering.Differentiation Mathlib.MeasureTheory.Covering.LiminfLimsup Mathlib.MeasureTheory.Covering.OneDim Mathlib.MeasureTheory.Covering.VitaliFamily Mathlib.MeasureTheory.Covering.Vitali Mathlib.MeasureTheory.Decomposition.Exhaustion Mathlib.MeasureTheory.Decomposition.IntegralRNDeriv Mathlib.MeasureTheory.Decomposition.Jordan Mathlib.MeasureTheory.Decomposition.Lebesgue Mathlib.MeasureTheory.Decomposition.RadonNikodym Mathlib.MeasureTheory.Decomposition.SignedHahn Mathlib.MeasureTheory.Decomposition.SignedLebesgue Mathlib.MeasureTheory.Decomposition.UnsignedHahn Mathlib.MeasureTheory.Function.AEEqFun.DomAct Mathlib.MeasureTheory.Function.AEEqOfIntegral Mathlib.MeasureTheory.Function.AEMeasurableOrder Mathlib.MeasureTheory.Function.AEMeasurableSequence Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator Mathlib.MeasureTheory.Function.ConditionalExpectation.Real Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique Mathlib.MeasureTheory.Function.ContinuousMapDense Mathlib.MeasureTheory.Function.EssSup Mathlib.MeasureTheory.Function.Floor Mathlib.MeasureTheory.Function.Intersectivity Mathlib.MeasureTheory.Function.Jacobian Mathlib.MeasureTheory.Function.L1Space.AEEqFun Mathlib.MeasureTheory.Function.L1Space.Integrable Mathlib.MeasureTheory.Function.L2Space Mathlib.MeasureTheory.Function.LocallyIntegrable Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic Mathlib.MeasureTheory.Function.LpSpace.DomAct.Continuous Mathlib.MeasureTheory.Function.SimpleFuncDenseLp Mathlib.MeasureTheory.Function.SimpleFunc Mathlib.MeasureTheory.Function.SpecialFunctions.Inner Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp Mathlib.MeasureTheory.Function.UnifTight Mathlib.MeasureTheory.Function.UniformIntegrable Mathlib.MeasureTheory.Group.AEStabilizer Mathlib.MeasureTheory.Group.Action Mathlib.MeasureTheory.Group.AddCircle Mathlib.MeasureTheory.Group.Arithmetic Mathlib.MeasureTheory.Group.Defs Mathlib.MeasureTheory.Group.FundamentalDomain Mathlib.MeasureTheory.Group.GeometryOfNumbers Mathlib.MeasureTheory.Group.Integral Mathlib.MeasureTheory.Group.MeasurableEquiv Mathlib.MeasureTheory.Group.Pointwise Mathlib.MeasureTheory.Integral.Asymptotics Mathlib.MeasureTheory.Integral.Average Mathlib.MeasureTheory.Integral.Bochner Mathlib.MeasureTheory.Integral.BoundedContinuousFunction Mathlib.MeasureTheory.Integral.CircleIntegral Mathlib.MeasureTheory.Integral.CircleTransform Mathlib.MeasureTheory.Integral.DivergenceTheorem Mathlib.MeasureTheory.Integral.DominatedConvergence Mathlib.MeasureTheory.Integral.ExpDecay Mathlib.MeasureTheory.Integral.FundThmCalculus Mathlib.MeasureTheory.Integral.Gamma Mathlib.MeasureTheory.Integral.IntegrableOn Mathlib.MeasureTheory.Integral.IntegralEqImproper Mathlib.MeasureTheory.Integral.IntervalAverage Mathlib.MeasureTheory.Integral.IntervalIntegral Mathlib.MeasureTheory.Integral.Layercake Mathlib.MeasureTheory.Integral.PeakFunction Mathlib.MeasureTheory.Integral.Periodic Mathlib.MeasureTheory.Integral.Pi Mathlib.MeasureTheory.Integral.Prod Mathlib.MeasureTheory.Integral.SetIntegral Mathlib.MeasureTheory.Integral.SetToL1 Mathlib.MeasureTheory.Integral.TorusIntegral Mathlib.MeasureTheory.Integral.VitaliCaratheodory Mathlib.MeasureTheory.Measure.AEDisjoint Mathlib.MeasureTheory.Measure.AEMeasurable Mathlib.MeasureTheory.Measure.AbsolutelyContinuous Mathlib.MeasureTheory.Measure.Comap Mathlib.MeasureTheory.Measure.Content Mathlib.MeasureTheory.Measure.ContinuousPreimage Mathlib.MeasureTheory.Measure.Count Mathlib.MeasureTheory.Measure.DiracProba Mathlib.MeasureTheory.Measure.Dirac Mathlib.MeasureTheory.Measure.FiniteMeasureProd Mathlib.MeasureTheory.Measure.FiniteMeasure Mathlib.MeasureTheory.Measure.Haar.Disintegration Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace Mathlib.MeasureTheory.Measure.Haar.NormedSpace Mathlib.MeasureTheory.Measure.Haar.OfBasis Mathlib.MeasureTheory.Measure.Haar.Quotient Mathlib.MeasureTheory.Measure.Haar.Unique Mathlib.MeasureTheory.Measure.Hausdorff Mathlib.MeasureTheory.Measure.Lebesgue.Basic Mathlib.MeasureTheory.Measure.Lebesgue.Complex Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar Mathlib.MeasureTheory.Measure.Lebesgue.Integral Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls Mathlib.MeasureTheory.Measure.LevyProkhorovMetric Mathlib.MeasureTheory.Measure.LogLikelihoodRatio Mathlib.MeasureTheory.Measure.Map Mathlib.MeasureTheory.Measure.MeasureSpaceDef Mathlib.MeasureTheory.Measure.MeasureSpace Mathlib.MeasureTheory.Measure.MutuallySingular Mathlib.MeasureTheory.Measure.NullMeasurable Mathlib.MeasureTheory.Measure.OpenPos Mathlib.MeasureTheory.Measure.Portmanteau Mathlib.MeasureTheory.Measure.ProbabilityMeasure Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving Mathlib.MeasureTheory.Measure.Regular Mathlib.MeasureTheory.Measure.RegularityCompacts Mathlib.MeasureTheory.Measure.Restrict Mathlib.MeasureTheory.Measure.SeparableMeasure Mathlib.MeasureTheory.Measure.Stieltjes Mathlib.MeasureTheory.Measure.Sub Mathlib.MeasureTheory.Measure.Tilted Mathlib.MeasureTheory.Measure.Trim Mathlib.MeasureTheory.Measure.Typeclasses Mathlib.MeasureTheory.Measure.WithDensityFinite Mathlib.MeasureTheory.Order.Group.Lattice Mathlib.MeasureTheory.Order.Lattice Mathlib.MeasureTheory.Order.UpperLower Mathlib.MeasureTheory.OuterMeasure.Caratheodory Mathlib.MeasureTheory.OuterMeasure.Induced Mathlib.MeasureTheory.OuterMeasure.OfFunction Mathlib.MeasureTheory.VectorMeasure.Basic Mathlib.MeasureTheory.VectorMeasure.WithDensity Mathlib.ModelTheory.Algebra.Field.CharP Mathlib.ModelTheory.Algebra.Field.IsAlgClosed Mathlib.ModelTheory.Algebra.Ring.Definability Mathlib.ModelTheory.Algebra.Ring.FreeCommRing Mathlib.NumberTheory.AbelSummation Mathlib.NumberTheory.Bertrand Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree Mathlib.NumberTheory.EulerProduct.ExpLog Mathlib.NumberTheory.FLT.Four Mathlib.NumberTheory.Harmonic.Bounds Mathlib.NumberTheory.Harmonic.EulerMascheroni Mathlib.NumberTheory.Harmonic.GammaDeriv Mathlib.NumberTheory.Harmonic.ZetaAsymp Mathlib.NumberTheory.KummerDedekind Mathlib.NumberTheory.LSeries.AbstractFuncEq Mathlib.NumberTheory.LSeries.Basic Mathlib.NumberTheory.LSeries.Convergence Mathlib.NumberTheory.LSeries.Convolution Mathlib.NumberTheory.LSeries.Deriv Mathlib.NumberTheory.LSeries.HurwitzZetaEven Mathlib.NumberTheory.LSeries.HurwitzZetaOdd Mathlib.NumberTheory.LSeries.HurwitzZetaValues Mathlib.NumberTheory.LSeries.HurwitzZeta Mathlib.NumberTheory.LSeries.Injectivity Mathlib.NumberTheory.LSeries.Linearity Mathlib.NumberTheory.LSeries.MellinEqDirichlet Mathlib.NumberTheory.LSeries.Positivity Mathlib.NumberTheory.LSeries.RiemannZeta Mathlib.NumberTheory.LSeries.SumCoeff Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable Mathlib.NumberTheory.Padics.Hensel Mathlib.NumberTheory.Padics.MahlerBasis Mathlib.NumberTheory.Padics.PadicIntegers Mathlib.NumberTheory.Padics.ProperSpace Mathlib.NumberTheory.Padics.RingHoms Mathlib.NumberTheory.Pell Mathlib.NumberTheory.PythagoreanTriples Mathlib.NumberTheory.RamificationInertia.Basic Mathlib.NumberTheory.SiegelsLemma Mathlib.NumberTheory.Transcendental.Lindemann.Init.AnalyticalPart Mathlib.NumberTheory.Transcendental.Liouville.Basic Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith Mathlib.NumberTheory.Transcendental.Liouville.Measure Mathlib.NumberTheory.Transcendental.Liouville.Residual Mathlib.NumberTheory.WellApproximable Mathlib.NumberTheory.ZetaValues Mathlib.Order.Filter.ZeroAndBoundedAtFilter Mathlib.Probability.BorelCantelli Mathlib.Probability.CDF Mathlib.Probability.CondVar Mathlib.Probability.ConditionalExpectation Mathlib.Probability.ConditionalProbability Mathlib.Probability.Density Mathlib.Probability.Distributions.Exponential Mathlib.Probability.Distributions.Gamma Mathlib.Probability.Distributions.Gaussian Mathlib.Probability.Distributions.Pareto Mathlib.Probability.Distributions.Uniform Mathlib.Probability.IdentDistrib Mathlib.Probability.Independence.Conditional Mathlib.Probability.Independence.Integrable Mathlib.Probability.Independence.ZeroOne Mathlib.Probability.Integration Mathlib.Probability.Kernel.Composition.IntegralCompProd Mathlib.Probability.Kernel.Composition.Lemmas Mathlib.Probability.Kernel.Composition.MeasureCompProd Mathlib.Probability.Kernel.Composition.MeasureComp Mathlib.Probability.Kernel.CondDistrib Mathlib.Probability.Kernel.Condexp Mathlib.Probability.Kernel.Disintegration.Basic Mathlib.Probability.Kernel.Disintegration.CDFToKernel Mathlib.Probability.Kernel.Disintegration.CondCDF Mathlib.Probability.Kernel.Disintegration.Density Mathlib.Probability.Kernel.Disintegration.Integral Mathlib.Probability.Kernel.Disintegration.StandardBorel Mathlib.Probability.Kernel.Disintegration.Unique Mathlib.Probability.Kernel.Integral Mathlib.Probability.Kernel.MeasurableIntegral Mathlib.Probability.Kernel.RadonNikodym Mathlib.Probability.Kernel.WithDensity Mathlib.Probability.Martingale.Basic Mathlib.Probability.Martingale.BorelCantelli Mathlib.Probability.Martingale.Centering Mathlib.Probability.Martingale.Convergence Mathlib.Probability.Martingale.OptionalSampling Mathlib.Probability.Martingale.OptionalStopping Mathlib.Probability.Martingale.Upcrossing Mathlib.Probability.Moments.Basic Mathlib.Probability.Moments.ComplexMGF Mathlib.Probability.Moments.IntegrableExpMul Mathlib.Probability.Moments.MGFAnalytic Mathlib.Probability.Notation Mathlib.Probability.ProbabilityMassFunction.Basic Mathlib.Probability.ProbabilityMassFunction.Binomial Mathlib.Probability.ProbabilityMassFunction.Constructions Mathlib.Probability.ProbabilityMassFunction.Integrals Mathlib.Probability.ProbabilityMassFunction.Monad Mathlib.Probability.Process.Adapted Mathlib.Probability.Process.Filtration Mathlib.Probability.Process.HittingTime Mathlib.Probability.Process.PartitionFiltration Mathlib.Probability.Process.Stopping Mathlib.Probability.StrongLaw Mathlib.Probability.UniformOn Mathlib.Probability.Variance Mathlib.RepresentationTheory.Character Mathlib.RepresentationTheory.FDRep Mathlib.RepresentationTheory.GroupCohomology.Basic Mathlib.RepresentationTheory.GroupCohomology.Hilbert90 Mathlib.RepresentationTheory.GroupCohomology.LowDegree Mathlib.RepresentationTheory.GroupCohomology.Resolution Mathlib.RepresentationTheory.Invariants Mathlib.RepresentationTheory.Rep Mathlib.RingTheory.Adjoin.Field Mathlib.RingTheory.Adjoin.PowerBasis Mathlib.RingTheory.AdjoinRoot Mathlib.RingTheory.Algebraic.Integral Mathlib.RingTheory.AlgebraicIndependent.Adjoin Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis Mathlib.RingTheory.ClassGroup Mathlib.RingTheory.DedekindDomain.AdicValuation Mathlib.RingTheory.DedekindDomain.Basic Mathlib.RingTheory.DedekindDomain.Factorization Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing Mathlib.RingTheory.DedekindDomain.Ideal Mathlib.RingTheory.DedekindDomain.SInteger Mathlib.RingTheory.DedekindDomain.SelmerGroup Mathlib.RingTheory.Derivation.MapCoeffs Mathlib.RingTheory.Flat.Basic Mathlib.RingTheory.Flat.CategoryTheory Mathlib.RingTheory.Flat.Equalizer Mathlib.RingTheory.Flat.EquationalCriterion Mathlib.RingTheory.Flat.FaithfullyFlat.Basic Mathlib.RingTheory.Flat.Localization Mathlib.RingTheory.Flat.Stability Mathlib.RingTheory.FreeCommRing Mathlib.RingTheory.Ideal.Over Mathlib.RingTheory.IntegralClosure.Algebra.Basic Mathlib.RingTheory.IntegralClosure.IntegrallyClosed Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic Mathlib.RingTheory.IsAdjoinRoot Mathlib.RingTheory.Jacobson.Ring Mathlib.RingTheory.LaurentSeries Mathlib.RingTheory.LinearDisjoint Mathlib.RingTheory.LocalProperties.IntegrallyClosed Mathlib.RingTheory.LocalRing.Quotient Mathlib.RingTheory.Localization.Away.AdjoinRoot Mathlib.RingTheory.Localization.Integral Mathlib.RingTheory.MvPolynomial.FreeCommRing Mathlib.RingTheory.MvPowerSeries.PiTopology Mathlib.RingTheory.Norm.Defs Mathlib.RingTheory.Norm.Transitivity Mathlib.RingTheory.Nullstellensatz Mathlib.RingTheory.Perfection Mathlib.RingTheory.Polynomial.GaussLemma Mathlib.RingTheory.Polynomial.Hermite.Gaussian Mathlib.RingTheory.Polynomial.RationalRoot Mathlib.RingTheory.Polynomial.SeparableDegree Mathlib.RingTheory.PowerBasis Mathlib.RingTheory.PowerSeries.PiTopology Mathlib.RingTheory.RingHom.FinitePresentation Mathlib.RingTheory.RingHom.Flat Mathlib.RingTheory.RingHom.Integral Mathlib.RingTheory.Spectrum.Maximal.Topology Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC Mathlib.RingTheory.Spectrum.Prime.Jacobson Mathlib.RingTheory.Spectrum.Prime.Module Mathlib.RingTheory.Spectrum.Prime.Noetherian Mathlib.RingTheory.Spectrum.Prime.Polynomial Mathlib.RingTheory.Spectrum.Prime.TensorProduct Mathlib.RingTheory.Spectrum.Prime.Topology Mathlib.RingTheory.TensorProduct.Nontrivial Mathlib.RingTheory.Valuation.AlgebraInstances Mathlib.RingTheory.Valuation.Integral Mathlib.RingTheory.Valuation.LocalSubring Mathlib.RingTheory.Valuation.Minpoly Mathlib.RingTheory.ZMod Mathlib.SetTheory.Cardinal.Free Mathlib.Tactic.FunProp.ContDiff Mathlib.Tactic.FunProp.Differentiable Mathlib.Tactic.ReduceModChar Mathlib.Topology.Algebra.Algebra.Equiv Mathlib.Topology.Algebra.Algebra Mathlib.Topology.Algebra.ContinuousAffineMap Mathlib.Topology.Algebra.ContinuousMonoidHom Mathlib.Topology.Algebra.FilterBasis Mathlib.Topology.Algebra.Group.Quotient Mathlib.Topology.Algebra.Group.TopologicalAbelianization Mathlib.Topology.Algebra.InfiniteSum.Module Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean Mathlib.Topology.Algebra.LinearTopology Mathlib.Topology.Algebra.Module.Alternating.Basic Mathlib.Topology.Algebra.Module.Basic Mathlib.Topology.Algebra.Module.CharacterSpace Mathlib.Topology.Algebra.Module.Determinant Mathlib.Topology.Algebra.Module.Equiv Mathlib.Topology.Algebra.Module.FiniteDimension Mathlib.Topology.Algebra.Module.LinearMapPiProd Mathlib.Topology.Algebra.Module.LinearMap Mathlib.Topology.Algebra.Module.LinearPMap Mathlib.Topology.Algebra.Module.LocallyConvex Mathlib.Topology.Algebra.Module.ModuleTopology Mathlib.Topology.Algebra.Module.Multilinear.Basic Mathlib.Topology.Algebra.Module.Simple Mathlib.Topology.Algebra.Module.Star Mathlib.Topology.Algebra.Module.WeakDual Mathlib.Topology.Algebra.NonUnitalAlgebra Mathlib.Topology.Algebra.NonUnitalStarAlgebra Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology Mathlib.Topology.Algebra.Nonarchimedean.Bases Mathlib.Topology.Algebra.Nonarchimedean.Basic Mathlib.Topology.Algebra.Nonarchimedean.Completion Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected Mathlib.Topology.Algebra.OpenSubgroup Mathlib.Topology.Algebra.Polynomial Mathlib.Topology.Algebra.Ring.Ideal Mathlib.Topology.Algebra.SeparationQuotient.Basic Mathlib.Topology.Algebra.SeparationQuotient.Section Mathlib.Topology.Algebra.StarSubalgebra Mathlib.Topology.Algebra.TopologicallyNilpotent Mathlib.Topology.Algebra.UniformField Mathlib.Topology.Algebra.UniformFilterBasis Mathlib.Topology.Algebra.UniformGroup.Basic Mathlib.Topology.Algebra.UniformRing Mathlib.Topology.Algebra.Valued.LocallyCompact Mathlib.Topology.Algebra.Valued.NormedValued Mathlib.Topology.Algebra.Valued.ValuationTopology Mathlib.Topology.Algebra.Valued.ValuedField Mathlib.Topology.Baire.BaireMeasurable Mathlib.Topology.Baire.CompleteMetrizable Mathlib.Topology.CWComplex Mathlib.Topology.Category.Profinite.Nobeling Mathlib.Topology.Category.TopCat.Sphere Mathlib.Topology.ContinuousMap.Algebra Mathlib.Topology.ContinuousMap.Lattice Mathlib.Topology.ContinuousMap.LocallyConstant Mathlib.Topology.ContinuousMap.Polynomial Mathlib.Topology.ContinuousMap.Star Mathlib.Topology.ContinuousMap.StoneWeierstrass Mathlib.Topology.ContinuousMap.Weierstrass Mathlib.Topology.Instances.Complex Mathlib.Topology.Instances.Irrational Mathlib.Topology.Instances.Matrix Mathlib.Topology.Instances.RatLemmas Mathlib.Topology.Instances.RealVectorSpace Mathlib.Topology.Instances.TrivSqZeroExt Mathlib.Topology.Instances.ZMultiples Mathlib.Topology.MetricSpace.Algebra Mathlib.Topology.MetricSpace.CantorScheme Mathlib.Topology.MetricSpace.Closeds Mathlib.Topology.MetricSpace.Completion Mathlib.Topology.MetricSpace.Contracting Mathlib.Topology.MetricSpace.HausdorffDimension Mathlib.Topology.MetricSpace.HausdorffDistance Mathlib.Topology.MetricSpace.Perfect Mathlib.Topology.MetricSpace.PiNat Mathlib.Topology.MetricSpace.Polish Mathlib.Topology.MetricSpace.Thickening Mathlib.Topology.Sheaves.CommRingCat Mathlib.Topology.Sheaves.MayerVietoris Mathlib.Topology.UniformSpace.Dini Mathlib.Topology.UniformSpace.Matrix	-1
Mathlib.GroupTheory.Schreier	1
Mathlib.GroupTheory.Commutator.Finite	24

---

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/declarations_diff.sh <optional_commit>

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

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

---

No changes to technical debt.

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

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• chore(GroupTheory/Commutator): don't import Ring #21296
  By Dependent Issues (🤖). Happy coding!