Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - chore: don't import algebra in Data.Finset.Basic #19779

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - chore: don't import algebra in Data.Finset.Basic #19779

wants to merge 1 commit into from
+69 −58

Conversation

YaelDillies
Copy link
Collaborator

@YaelDillies YaelDillies commented Dec 7, 2024 •
edited
Loading

@YaelDillies YaelDillies added the t-data Data (lists, quotients, numbers, etc) label Dec 7, 2024
@github-actions GitHub Actions
Copy link

github-actions bot commented Dec 7, 2024 •
edited
Loading

PR summary 86d5e52fc4

Import changes for modified files

Dependency changes

File Base Count Head Count Change
Mathlib.Data.Multiset.Range 372 359 -13 (-3.49%)
Mathlib.Data.Multiset.Nodup 374 361 -13 (-3.48%)
Mathlib.Data.Finset.Defs 375 362 -13 (-3.47%)
Mathlib.Data.Multiset.Dedup 376 363 -13 (-3.46%)
Mathlib.Data.Multiset.NatAntidiagonal 376 363 -13 (-3.46%)
Mathlib.Data.Finset.Disjoint 384 371 -13 (-3.39%)
Mathlib.Data.Finset.Lattice.Lemmas 385 372 -13 (-3.38%)
Mathlib.Data.Finset.Basic 395 382 -13 (-3.29%)
Mathlib.Algebra.Order.Group.Multiset 371 376 +5 (+1.35%)
Mathlib.Data.Multiset.Sum 375 377 +2 (+0.53%)
Mathlib.Data.Finsupp.Multiset 716 717 +1 (+0.14%)
Mathlib.RingTheory.Radical 723 724 +1 (+0.14%)
Mathlib.Algebra.Polynomial.FieldDivision 1090 1091 +1 (+0.09%)
Import changes for all files
Files Import difference
23 files Mathlib.Data.Multiset.Nodup Mathlib.Data.Multiset.NatAntidiagonal Mathlib.Data.Finset.Defs Mathlib.Data.Finset.Insert Mathlib.Data.Finset.Dedup Mathlib.Data.Finset.SDiff Mathlib.Data.Set.Constructions Mathlib.Data.Finset.Lattice.Basic Mathlib.Data.Finset.Erase Mathlib.Data.Finset.Update Mathlib.Data.Finset.Disjoint Mathlib.Data.Multiset.FinsetOps Mathlib.Data.Finset.Order Mathlib.Data.Finset.Filter Mathlib.Data.Multiset.Range Mathlib.Data.Finset.Empty Mathlib.Data.Finset.Basic Mathlib.Data.Multiset.Sort Mathlib.Data.Finset.Lattice.Lemmas Mathlib.Data.Finset.SymmDiff Mathlib.Data.Finset.Attach Mathlib.Data.Finset.Range Mathlib.Data.Multiset.Dedup
 -13
Mathlib.Algebra.FreeMonoid.Symbols -5
1293 files Mathlib.LinearAlgebra.FreeModule.Norm Mathlib.LinearAlgebra.Charpoly.Basic Mathlib.NumberTheory.NumberField.Discriminant.Defs Mathlib.MeasureTheory.Integral.VitaliCaratheodory Mathlib.RingTheory.FractionalIdeal.Norm Mathlib.Algebra.Polynomial.FieldDivision Mathlib.Analysis.MeanInequalitiesPow Mathlib.Topology.Algebra.Module.Simple Mathlib.Combinatorics.Additive.ErdosGinzburgZiv Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion Mathlib.RingTheory.IsAdjoinRoot Mathlib.AlgebraicGeometry.Modules.Sheaf Mathlib.Combinatorics.SimpleGraph.Triangle.Removal Mathlib.Analysis.BoxIntegral.UnitPartition Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs Mathlib.Analysis.CStarAlgebra.GelfandDuality Mathlib.Probability.Process.HittingTime Mathlib.NumberTheory.RamificationInertia.Basic Mathlib.Analysis.InnerProductSpace.Spectrum Mathlib.Analysis.InnerProductSpace.Symmetric Mathlib.Analysis.InnerProductSpace.OfNorm Mathlib.NumberTheory.Cyclotomic.Rat Mathlib.RingTheory.DedekindDomain.Dvr Mathlib.RingTheory.Henselian Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Symmetric Mathlib.FieldTheory.IsPerfectClosure Mathlib.Probability.BorelCantelli Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv Mathlib.NumberTheory.Wilson Mathlib.Geometry.Manifold.ContMDiff.Atlas Mathlib.RingTheory.Polynomial.Content Mathlib.RepresentationTheory.GroupCohomology.Hilbert90 Mathlib.Dynamics.TopologicalEntropy.NetEntropy Mathlib.NumberTheory.LSeries.HurwitzZetaValues Mathlib.RingTheory.PowerBasis Mathlib.Analysis.SpecialFunctions.Gamma.Basic Mathlib.Geometry.Manifold.VectorBundle.Pullback Mathlib.FieldTheory.Finite.Trace Mathlib.NumberTheory.Padics.MahlerBasis Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith Mathlib.AlgebraicGeometry.Sites.Etale Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual Mathlib.LinearAlgebra.Matrix.ZPow Mathlib.Analysis.Convex.AmpleSet Mathlib.Probability.Variance Mathlib.Analysis.Complex.Angle Mathlib.LinearAlgebra.Matrix.PosDef Mathlib.RingTheory.SimpleModule Mathlib.Algebra.Category.FGModuleCat.Limits Mathlib.Analysis.SpecialFunctions.Integrals Mathlib.NumberTheory.Harmonic.ZetaAsymp Mathlib.Dynamics.Ergodic.AddCircle Mathlib.Analysis.Calculus.BumpFunction.Convolution Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem Mathlib.Analysis.Fourier.PoissonSummation Mathlib.AlgebraicGeometry.Morphisms.Proper Mathlib.Analysis.InnerProductSpace.Rayleigh Mathlib.Analysis.Normed.Module.Dual Mathlib.LinearAlgebra.ExteriorAlgebra.Grading Mathlib.NumberTheory.NumberField.Discriminant.Basic Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms Mathlib.NumberTheory.Cyclotomic.Discriminant Mathlib.NumberTheory.MulChar.Lemmas Mathlib.AlgebraicGeometry.Morphisms.Preimmersion Mathlib.RingTheory.PowerSeries.WellKnown Mathlib.Geometry.Manifold.VectorBundle.Basic Mathlib.Analysis.Calculus.Deriv.Abs Mathlib.Analysis.CStarAlgebra.Multiplier Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds Mathlib.Analysis.SpecialFunctions.Pow.Complex Mathlib.MeasureTheory.Measure.FiniteMeasure Mathlib.Tactic.FunProp.ContDiff Mathlib.AlgebraicGeometry.PrimeSpectrum.TensorProduct Mathlib.MeasureTheory.Function.SpecialFunctions.Basic Mathlib.MeasureTheory.Integral.IntervalAverage Mathlib.Analysis.Distribution.FourierSchwartz Mathlib.Analysis.Normed.Lp.PiLp Mathlib.RingTheory.WittVector.Domain Mathlib.Analysis.Calculus.ParametricIntervalIntegral Mathlib.MeasureTheory.Measure.ProbabilityMeasure Mathlib.Geometry.Manifold.VectorBundle.Tangent Mathlib.LinearAlgebra.Matrix.MvPolynomial Mathlib.FieldTheory.Laurent Mathlib.MeasureTheory.Function.UnifTight Mathlib.Analysis.SpecialFunctions.CompareExp Mathlib.NumberTheory.GaussSum Mathlib.RingTheory.AlgebraicIndependent.Transcendental Mathlib.Geometry.Manifold.Diffeomorph Mathlib.LinearAlgebra.Dimension.DivisionRing Mathlib.LinearAlgebra.FreeModule.StrongRankCondition Mathlib.Combinatorics.Additive.Corner.Roth Mathlib.MeasureTheory.Function.LpSeminorm.Basic Mathlib.MeasureTheory.Measure.Lebesgue.Complex Mathlib.LinearAlgebra.BilinearForm.DualLattice Mathlib.NumberTheory.EulerProduct.DirichletLSeries Mathlib.RingTheory.DedekindDomain.Ideal Mathlib.Analysis.SpecialFunctions.Complex.Log Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology Mathlib.MeasureTheory.Integral.IntervalIntegral Mathlib.Topology.ContinuousMap.Polynomial Mathlib.Analysis.Calculus.FDeriv.WithLp Mathlib.AlgebraicGeometry.Sites.MorphismProperty Mathlib.Analysis.Complex.AbsMax Mathlib.AlgebraicGeometry.Sites.BigZariski Mathlib.RingTheory.Ideal.Over Mathlib.RingTheory.Flat.Basic Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter Mathlib.Analysis.InnerProductSpace.ProdL2 Mathlib.Probability.Kernel.Disintegration.CDFToKernel Mathlib.RingTheory.LocalRing.Quotient Mathlib.Algebra.Category.ModuleCat.Differentials.Basic Mathlib.Data.Real.GoldenRatio Mathlib.RingTheory.WittVector.InitTail Mathlib.Geometry.Manifold.MFDeriv.Basic Mathlib.Analysis.CStarAlgebra.Spectrum Mathlib.LinearAlgebra.Dimension.Localization Mathlib.Geometry.Manifold.Instances.Real Mathlib.RingTheory.Localization.NormTrace Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv Mathlib.LinearAlgebra.Lagrange Mathlib.Geometry.Manifold.Complex Mathlib.Logic.Hydra Mathlib.LinearAlgebra.Coevaluation Mathlib.FieldTheory.AbelRuffini Mathlib.RingTheory.ClassGroup Mathlib.AlgebraicGeometry.Morphisms.Basic Mathlib.NumberTheory.LSeries.DirichletContinuation Mathlib.MeasureTheory.Integral.CircleIntegral Mathlib.Probability.StrongLaw Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital Mathlib.RingTheory.Regular.RegularSequence Mathlib.Analysis.Normed.Module.FiniteDimension Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique Mathlib.NumberTheory.NumberField.FractionalIdeal Mathlib.LinearAlgebra.Matrix.Diagonal Mathlib.RingTheory.TensorProduct.Nontrivial Mathlib.AlgebraicGeometry.Morphisms.IsIso Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral Mathlib.AlgebraicGeometry.Modules.Presheaf Mathlib.RingTheory.MvPowerSeries.LexOrder Mathlib.RingTheory.Algebraic.MvPolynomial Mathlib.Probability.Kernel.Composition.MeasureCompProd Mathlib.Algebra.Module.DedekindDomain Mathlib.RingTheory.Trace.Defs Mathlib.RingTheory.WittVector.Compare Mathlib.Probability.Kernel.Composition.IntegralCompProd Mathlib.Algebra.MvPolynomial.Counit Mathlib.LinearAlgebra.Eigenspace.Matrix Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid Mathlib.Analysis.SpecialFunctions.Gamma.Beta Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure Mathlib.MeasureTheory.Integral.TorusIntegral Mathlib.Algebra.MvPolynomial.Basic Mathlib.Analysis.Complex.Isometry Mathlib.RingTheory.Adjoin.PowerBasis Mathlib.Geometry.Manifold.MFDeriv.FDeriv Mathlib.Analysis.Convex.Side Mathlib.NumberTheory.ArithmeticFunction Mathlib.MeasureTheory.Function.L2Space Mathlib.AlgebraicGeometry.PrimeSpectrum.FreeLocus Mathlib.MeasureTheory.Measure.LevyProkhorovMetric Mathlib.RingTheory.Polynomial.Quotient Mathlib.Algebra.Module.ZLattice.Covolume Mathlib.RingTheory.AdicCompletion.Functoriality Mathlib.Algebra.CharP.LocalRing Mathlib.LinearAlgebra.PID Mathlib.RingTheory.LaurentSeries Mathlib.NumberTheory.ModularForms.Identities Mathlib.MeasureTheory.Function.ContinuousMapDense Mathlib.Analysis.Complex.Periodic Mathlib.Analysis.Normed.Algebra.Norm Mathlib.Computability.AkraBazzi.GrowsPolynomially Mathlib.Geometry.Manifold.ContMDiffMap Mathlib.Algebra.MvPolynomial.Funext Mathlib.NumberTheory.NumberField.Norm Mathlib.Topology.Category.Profinite.Nobeling Mathlib.ModelTheory.Algebra.Ring.Definability Mathlib.LinearAlgebra.FreeModule.Determinant Mathlib.FieldTheory.Isaacs Mathlib.Analysis.Complex.TaylorSeries Mathlib.Analysis.Normed.Algebra.Spectrum Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions Mathlib.RingTheory.LocalRing.ResidueField.Ideal Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality Mathlib.Topology.Compactification.OnePointEquiv Mathlib.Analysis.FunctionalSpaces.SobolevInequality Mathlib.LinearAlgebra.QuadraticForm.Prod Mathlib.RingTheory.Trace.Basic Mathlib.SetTheory.Cardinal.Finsupp Mathlib.NumberTheory.LSeries.ZMod Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan Mathlib.Analysis.CStarAlgebra.Module.Constructions Mathlib.Probability.Distributions.Exponential Mathlib.RingTheory.WittVector.MulCoeff Mathlib.RingTheory.RingHom.FiniteType Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric Mathlib.Analysis.SpecialFunctions.Complex.Arctan Mathlib.RingTheory.Algebraic.Cardinality Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation Mathlib.Algebra.Lie.Nilpotent Mathlib.Analysis.BoxIntegral.Partition.Measure Mathlib.LinearAlgebra.Charpoly.ToMatrix Mathlib.FieldTheory.Normal Mathlib.RingTheory.KrullDimension.Field Mathlib.LinearAlgebra.FreeModule.IdealQuotient Mathlib.Analysis.Fourier.AddCircleMulti Mathlib.Probability.Martingale.Upcrossing Mathlib.MeasureTheory.Function.SimpleFuncDenseLp Mathlib.Analysis.RCLike.Lemmas Mathlib.Data.Nat.Choose.Lucas Mathlib.Algebra.Polynomial.Splits Mathlib.Probability.Martingale.OptionalSampling Mathlib.RingTheory.Norm.Defs Mathlib.RingTheory.Kaehler.Polynomial Mathlib.GroupTheory.Exponent Mathlib.Analysis.RCLike.Inner Mathlib.RingTheory.WittVector.Identities Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap Mathlib.Analysis.Convex.GaugeRescale Mathlib.LinearAlgebra.RootSystem.RootPairingCat Mathlib.FieldTheory.Minpoly.Basic Mathlib.FieldTheory.Adjoin Mathlib.MeasureTheory.Integral.DivergenceTheorem Mathlib.LinearAlgebra.ExteriorPower.Basic Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact Mathlib.Analysis.SpecialFunctions.Log.NegMulLog Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion Mathlib.Analysis.Calculus.BumpFunction.Basic Mathlib.NumberTheory.NumberField.EquivReindex Mathlib.Algebra.MvPolynomial.Expand Mathlib.RepresentationTheory.GroupCohomology.Resolution Mathlib.LinearAlgebra.Matrix.Gershgorin Mathlib.RingTheory.Localization.Integral Mathlib.AlgebraicGeometry.Morphisms.Integral Mathlib.Algebra.Lie.Derivation.Killing Mathlib.RingTheory.AdicCompletion.Exactness Mathlib.MeasureTheory.Measure.LogLikelihoodRatio Mathlib.FieldTheory.SeparableClosure Mathlib.Data.ZMod.Quotient Mathlib.RingTheory.WittVector.Truncated Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots Mathlib.Data.Nat.Squarefree Mathlib.NumberTheory.SiegelsLemma Mathlib.LinearAlgebra.JordanChevalley Mathlib.Analysis.SpecialFunctions.ImproperIntegrals Mathlib.AlgebraicGeometry.Noetherian Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties Mathlib.Data.Nat.Factorization.Induction Mathlib.Analysis.InnerProductSpace.Dual Mathlib.FieldTheory.ChevalleyWarning Mathlib.RingTheory.Polynomial.Hermite.Gaussian Mathlib.FieldTheory.IsAlgClosed.Classification Mathlib.LinearAlgebra.QuadraticForm.Basic Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary Mathlib.Analysis.Calculus.AddTorsor.Coord Mathlib.LinearAlgebra.QuadraticForm.Basis Mathlib.RepresentationTheory.Rep Mathlib.AlgebraicGeometry.EllipticCurve.Affine Mathlib.AlgebraicGeometry.EllipticCurve.Group Mathlib.RingTheory.RingHom.StandardSmooth Mathlib.NumberTheory.SumPrimeReciprocals Mathlib.Data.Finsupp.Weight Mathlib.RingTheory.RingHom.Flat Mathlib.MeasureTheory.Function.LpSeminorm.Trim Mathlib.Analysis.PSeries Mathlib.Algebra.Module.Presentation.Differentials Mathlib.Analysis.Fourier.ZMod Mathlib.Analysis.SpecialFunctions.Complex.LogBounds Mathlib.MeasureTheory.Function.LpSpace Mathlib.NumberTheory.ModularForms.SlashActions Mathlib.Analysis.SpecialFunctions.Gamma.Deligne Mathlib.Analysis.Complex.PhragmenLindelof Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity Mathlib.Algebra.CubicDiscriminant Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat Mathlib.Analysis.Calculus.SmoothSeries Mathlib.GroupTheory.Nilpotent Mathlib.RingTheory.WittVector.WittPolynomial Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff Mathlib.GroupTheory.CommutingProbability Mathlib.Analysis.InnerProductSpace.NormPow Mathlib.Algebra.Module.ZLattice.Basic Mathlib.Analysis.Convex.Intrinsic Mathlib.LinearAlgebra.BilinearForm.Orthogonal Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls Mathlib.RingTheory.Invariant Mathlib.AlgebraicGeometry.Sites.Small Mathlib.MeasureTheory.Integral.FundThmCalculus Mathlib.AlgebraicGeometry.Spec Mathlib.NumberTheory.Cyclotomic.Three Mathlib.Probability.Kernel.Disintegration.Integral Mathlib.NumberTheory.LSeries.HurwitzZetaEven Mathlib.RingTheory.Unramified.Field Mathlib.Analysis.CStarAlgebra.Matrix Mathlib.RingTheory.AlgebraicIndependent.Defs Mathlib.RingTheory.EssentialFiniteness Mathlib.FieldTheory.IntermediateField.Algebraic Mathlib.Algebra.GCDMonoid.IntegrallyClosed Mathlib.LinearAlgebra.PerfectPairing Mathlib.NumberTheory.DirichletCharacter.Orthogonality Mathlib.RingTheory.Regular.IsSMulRegular Mathlib.FieldTheory.SeparableDegree Mathlib.Geometry.Manifold.PoincareConjecture Mathlib.FieldTheory.Minpoly.MinpolyDiv Mathlib.RingTheory.MvPolynomial.Symmetric.Defs Mathlib.MeasureTheory.Measure.Portmanteau Mathlib.RingTheory.PowerSeries.Derivative Mathlib.NumberTheory.LSeries.Deriv Mathlib.AlgebraicGeometry.ResidueField Mathlib.MeasureTheory.Measure.Haar.NormedSpace Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective Mathlib.RingTheory.Ideal.Cotangent Mathlib.NumberTheory.EulerProduct.Basic Mathlib.Analysis.Fourier.AddCircle Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation Mathlib.RingTheory.Flat.Localization Mathlib.RingTheory.Nullstellensatz Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar Mathlib.Analysis.SpecialFunctions.Pow.Continuity Mathlib.Analysis.Calculus.MeanValue Mathlib.GroupTheory.SchurZassenhaus Mathlib.Analysis.Calculus.LineDeriv.QuadraticMap Mathlib.Analysis.Fourier.Inversion Mathlib.Analysis.Normed.Algebra.QuaternionExponential Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality Mathlib.Computability.AkraBazzi.AkraBazzi Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly Mathlib.Algebra.Lie.CartanSubalgebra Mathlib.LinearAlgebra.Trace Mathlib.RingTheory.Polynomial.Radical Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow Mathlib.Algebra.Algebra.Subalgebra.Rank Mathlib.Topology.Instances.AddCircle Mathlib.AlgebraicGeometry.Over Mathlib.NumberTheory.NumberField.Completion Mathlib.Probability.Kernel.WithDensity Mathlib.Analysis.SpecialFunctions.NonIntegrable Mathlib.Geometry.Euclidean.Angle.Oriented.Basic Mathlib.FieldTheory.Galois.GaloisClosure Mathlib.Topology.Algebra.Valued.NormedValued Mathlib.LinearAlgebra.Matrix.FiniteDimensional Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities Mathlib.FieldTheory.Fixed Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic Mathlib.RingTheory.Adjoin.Field Mathlib.Data.Nat.Factorization.Defs Mathlib.Geometry.Euclidean.Sphere.Ptolemy Mathlib.AlgebraicGeometry.Pullbacks Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp Mathlib.FieldTheory.Finite.Basic Mathlib.Topology.Algebra.Module.FiniteDimension Mathlib.Algebra.Category.ModuleCat.Simple Mathlib.Analysis.Normed.Algebra.MatrixExponential Mathlib.RingTheory.IntegralClosure.IntegralRestrict Mathlib.Algebra.Category.Grp.EnoughInjectives Mathlib.Analysis.Calculus.Taylor Mathlib.MeasureTheory.Group.AddCircle Mathlib.Probability.Independence.ZeroOne Mathlib.Analysis.SpecialFunctions.Complex.Analytic Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree Mathlib.Combinatorics.SimpleGraph.Regularity.Increment Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic Mathlib.Algebra.Lie.TraceForm Mathlib.Analysis.LocallyConvex.WeakSpace Mathlib.Analysis.Calculus.LHopital Mathlib.Analysis.Convex.Cone.Pointed Mathlib.Probability.Kernel.Disintegration.StandardBorel Mathlib.MeasureTheory.Function.UniformIntegrable Mathlib.LinearAlgebra.RootSystem.OfBilinear Mathlib.MeasureTheory.Measure.Hausdorff Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf Mathlib.NumberTheory.ModularForms.SlashInvariantForms Mathlib.Geometry.Manifold.SmoothManifoldWithCorners Mathlib.FieldTheory.SplittingField.IsSplittingField Mathlib.FieldTheory.IsSepClosed Mathlib.Algebra.Lie.Killing Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup Mathlib.AlgebraicGeometry.PrimeSpectrum.Jacobson Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict Mathlib.Probability.Distributions.Gaussian Mathlib.NumberTheory.LSeries.Injectivity Mathlib.Probability.Kernel.CondDistrib Mathlib.RingTheory.Algebraic.Basic Mathlib.Analysis.SpecificLimits.FloorPow Mathlib.Analysis.Calculus.FDeriv.Measurable Mathlib.GroupTheory.GroupAction.Period Mathlib.Analysis.Calculus.UniformLimitsDeriv Mathlib.RingTheory.RootsOfUnity.Lemmas Mathlib.NumberTheory.ModularForms.LevelOne Mathlib.MeasureTheory.Integral.Bochner Mathlib.Algebra.Lie.Character Mathlib.Algebra.Order.AbsoluteValue.Equivalence Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart Mathlib.RingTheory.Presentation Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart Mathlib.MeasureTheory.Measure.Haar.Unique Mathlib.Geometry.Manifold.BumpFunction Mathlib.Analysis.Calculus.FDeriv.Extend Mathlib.RingTheory.MvPolynomial.Homogeneous Mathlib.Probability.Martingale.Basic Mathlib.Data.Finsupp.Antidiagonal Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho Mathlib.Algebra.Squarefree.Basic Mathlib.Algebra.Polynomial.Expand Mathlib.FieldTheory.Finite.Polynomial Mathlib.NumberTheory.Cyclotomic.Gal Mathlib.Geometry.Manifold.IntegralCurve.Basic Mathlib.LinearAlgebra.FiniteDimensional Mathlib.Analysis.Normed.Lp.ProdLp Mathlib.RingTheory.MvPolynomial.Ideal Mathlib.MeasureTheory.Decomposition.RadonNikodym Mathlib.Probability.Kernel.RadonNikodym Mathlib.RingTheory.Polynomial.Vieta Mathlib.RingTheory.Kaehler.CotangentComplex Mathlib.NumberTheory.Harmonic.GammaDeriv Mathlib.Geometry.Manifold.InteriorBoundary Mathlib.Analysis.InnerProductSpace.Subspace Mathlib.FieldTheory.Extension Mathlib.LinearAlgebra.Orientation Mathlib.LinearAlgebra.FreeModule.Int Mathlib.NumberTheory.LSeries.Basic Mathlib.Geometry.Manifold.ContMDiffMFDeriv Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone Mathlib.Analysis.Normed.Ring.SeminormFromConst Mathlib.MeasureTheory.Decomposition.SignedLebesgue Mathlib.NumberTheory.NumberField.ProductFormula Mathlib.NumberTheory.SumFourSquares Mathlib.LinearAlgebra.RootSystem.WeylGroup Mathlib.Combinatorics.Configuration Mathlib.AlgebraicGeometry.Properties Mathlib.Analysis.Convex.StrictConvexSpace Mathlib.Geometry.Manifold.ContMDiff.Basic Mathlib.MeasureTheory.Measure.WithDensityFinite Mathlib.RingTheory.Etale.Field Mathlib.Geometry.Euclidean.Sphere.Power Mathlib.Data.Real.Pi.Irrational Mathlib.RingTheory.PowerSeries.PiTopology Mathlib.RingTheory.FinitePresentation Mathlib.AlgebraicGeometry.Morphisms.Affine Mathlib.Analysis.Complex.CauchyIntegral Mathlib.LinearAlgebra.Semisimple Mathlib.FieldTheory.AbsoluteGaloisGroup Mathlib.LinearAlgebra.RootSystem.Basic Mathlib.Analysis.InnerProductSpace.JointEigenspace Mathlib.Algebra.Lie.Weights.Basic Mathlib.Algebra.Lie.Weights.RootSystem Mathlib.RingTheory.DividedPowers.Basic Mathlib.Analysis.SpecialFunctions.Pow.Deriv Mathlib.MeasureTheory.Group.GeometryOfNumbers Mathlib.Analysis.SpecialFunctions.PolarCoord Mathlib.AlgebraicGeometry.Morphisms.Immersion Mathlib.MeasureTheory.Covering.LiminfLimsup Mathlib.Geometry.Euclidean.Angle.Sphere Mathlib.Analysis.InnerProductSpace.LinearPMap Mathlib.Analysis.Complex.UpperHalfPlane.Topology Mathlib.Analysis.Complex.IsIntegral Mathlib.RepresentationTheory.Invariants Mathlib.RingTheory.Valuation.Integral Mathlib.FieldTheory.RatFunc.AsPolynomial Mathlib.RingTheory.Flat.CategoryTheory Mathlib.RingTheory.MvPolynomial.Localization Mathlib.Analysis.SpecialFunctions.Log.Base Mathlib.MeasureTheory.Order.UpperLower Mathlib.NumberTheory.Rayleigh Mathlib.Analysis.Calculus.ParametricIntegral Mathlib.MeasureTheory.Function.AEEqFun.DomAct Mathlib.Probability.Martingale.Convergence Mathlib.Analysis.Convex.SpecificFunctions.Pow Mathlib.FieldTheory.KrullTopology Mathlib.Analysis.Complex.UpperHalfPlane.Metric Mathlib.RingTheory.LittleWedderburn Mathlib.Analysis.Normed.Lp.lpSpace Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner Mathlib.Algebra.Category.ModuleCat.EnoughInjectives Mathlib.RingTheory.Unramified.Pi Mathlib.Algebra.Lie.LieTheorem Mathlib.RingTheory.Radical Mathlib.AlgebraicGeometry.Morphisms.Separated Mathlib.LinearAlgebra.TensorAlgebra.Basis Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable Mathlib.CategoryTheory.Preadditive.Schur Mathlib.Analysis.Normed.Ring.Seminorm Mathlib.Analysis.InnerProductSpace.Basic Mathlib.RingTheory.Generators Mathlib.RingTheory.Adjoin.Tower Mathlib.Algebra.Category.Ring.LinearAlgebra Mathlib.Probability.Kernel.Disintegration.CondCDF Mathlib.MeasureTheory.Function.AEEqOfIntegral Mathlib.Combinatorics.Extremal.RuzsaSzemeredi Mathlib.Data.Complex.Determinant Mathlib.Analysis.Complex.OperatorNorm Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov Mathlib.Analysis.PSeriesComplex Mathlib.RingTheory.Polynomial.HilbertPoly Mathlib.FieldTheory.Relrank Mathlib.Probability.Kernel.Disintegration.Density Mathlib.Analysis.Calculus.LagrangeMultipliers Mathlib.LinearAlgebra.BilinearForm.Properties Mathlib.RingTheory.MvPolynomial.FreeCommRing Mathlib.RingTheory.Polynomial.Cyclotomic.Basic Mathlib.RingTheory.Ideal.Norm.AbsNorm Mathlib.Analysis.InnerProductSpace.Completion Mathlib.Analysis.Convex.Integral Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace Mathlib.LinearAlgebra.FiniteDimensional.Defs Mathlib.AlgebraicGeometry.RationalMap Mathlib.AlgebraicGeometry.Modules.Tilde Mathlib.AlgebraicGeometry.Morphisms.Finite Mathlib.MeasureTheory.Function.SpecialFunctions.Arctan Mathlib.FieldTheory.Galois.Profinite Mathlib.RingTheory.Polynomial.Bernstein Mathlib.FieldTheory.LinearDisjoint Mathlib.AlgebraicGeometry.Cover.Over Mathlib.Algebra.LinearRecurrence Mathlib.AlgebraicGeometry.PrimeSpectrum.Noetherian Mathlib.RingTheory.Ideal.Norm.RelNorm Mathlib.LinearAlgebra.CliffordAlgebra.Star Mathlib.LinearAlgebra.Projectivization.Constructions Mathlib.RingTheory.DiscreteValuationRing.TFAE Mathlib.Algebra.MvPolynomial.Rename Mathlib.NumberTheory.MulChar.Duality Mathlib.MeasureTheory.Integral.Prod Mathlib.Algebra.Order.Antidiag.Nat Mathlib.NumberTheory.Cyclotomic.Embeddings Mathlib.MeasureTheory.Integral.Layercake Mathlib.RingTheory.ZMod Mathlib.Geometry.Euclidean.Circumcenter Mathlib.LinearAlgebra.Matrix.Nondegenerate Mathlib.Analysis.CStarAlgebra.Module.Defs Mathlib.Analysis.Complex.Schwarz Mathlib.NumberTheory.LegendreSymbol.Basic Mathlib.RingTheory.Adjoin.FG Mathlib.Analysis.Fourier.FourierTransformDeriv Mathlib.RingTheory.Polynomial.Cyclotomic.Roots Mathlib.RingTheory.FiniteStability Mathlib.RingTheory.Localization.InvSubmonoid Mathlib.Analysis.Complex.UpperHalfPlane.Manifold Mathlib.LinearAlgebra.TensorProduct.Matrix Mathlib.Analysis.SpecialFunctions.Complex.Arg Mathlib.FieldTheory.Finite.GaloisField Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic Mathlib.RepresentationTheory.Character Mathlib.AlgebraicGeometry.PrimeSpectrum.Module Mathlib.NumberTheory.SmoothNumbers Mathlib.RingTheory.RingHom.FinitePresentation Mathlib.Algebra.MvPolynomial.Derivation Mathlib.NumberTheory.LSeries.RiemannZeta Mathlib.MeasureTheory.Covering.OneDim Mathlib.Data.Real.Pi.Leibniz Mathlib.LinearAlgebra.QuadraticForm.Real Mathlib.LinearAlgebra.CliffordAlgebra.Equivs Mathlib.Algebra.MvPolynomial.Variables Mathlib.RingTheory.DedekindDomain.IntegralClosure Mathlib.RepresentationTheory.Basic Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing Mathlib.NumberTheory.FLT.Three Mathlib.FieldTheory.Galois.Basic Mathlib.RingTheory.WittVector.Verschiebung Mathlib.RingTheory.Filtration Mathlib.Geometry.Manifold.Algebra.SmoothFunctions Mathlib.Algebra.Lie.SkewAdjoint Mathlib.Geometry.Euclidean.Inversion.Calculus Mathlib.Analysis.Calculus.FirstDerivativeTest Mathlib.LinearAlgebra.LinearDisjoint Mathlib.Analysis.InnerProductSpace.Positive Mathlib.LinearAlgebra.CliffordAlgebra.Fold Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody Mathlib.LinearAlgebra.FreeModule.Finite.Matrix Mathlib.LinearAlgebra.Matrix.Charpoly.Basic Mathlib.Algebra.Lie.Weights.Chain Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital Mathlib.NumberTheory.NumberField.Units.Basic Mathlib.RingTheory.Algebraic.Integral Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral Mathlib.RingTheory.Valuation.RamificationGroup Mathlib.Probability.Distributions.Uniform Mathlib.RingTheory.MvPolynomial Mathlib.SetTheory.Surreal.Dyadic Mathlib.Geometry.Euclidean.Sphere.SecondInter Mathlib.Geometry.Euclidean.Basic Mathlib.Algebra.Lie.Matrix Mathlib.MeasureTheory.Covering.DensityTheorem Mathlib.Algebra.MvPolynomial.Supported Mathlib.RingTheory.MvPolynomial.Tower Mathlib.Analysis.Analytic.RadiusLiminf Mathlib.MeasureTheory.Constructions.UnitInterval Mathlib.Data.Matrix.Rank Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique Mathlib.GroupTheory.Torsion Mathlib.NumberTheory.DirichletCharacter.GaussSum Mathlib.Data.Finsupp.Multiset Mathlib.LinearAlgebra.QuadraticForm.Complex Mathlib.MeasureTheory.Measure.FiniteMeasureProd Mathlib.Geometry.Manifold.Sheaf.Smooth Mathlib.Geometry.Manifold.VectorBundle.Hom Mathlib.Analysis.InnerProductSpace.Orthogonal Mathlib.Probability.Kernel.MeasurableIntegral Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable Mathlib.Geometry.Euclidean.MongePoint Mathlib.Topology.CWComplex Mathlib.Analysis.Convex.Between Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional Mathlib.Algebra.AlgebraicCard Mathlib.Analysis.Calculus.ContDiff.Bounds Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds Mathlib.NumberTheory.Ostrowski Mathlib.Data.Real.Irrational Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic Mathlib.AlgebraicGeometry.SpreadingOut Mathlib.AlgebraicGeometry.StructureSheaf Mathlib.LinearAlgebra.Contraction Mathlib.MeasureTheory.Measure.Doubling Mathlib.RingTheory.MvPolynomial.EulerIdentity Mathlib.Analysis.MeanInequalities Mathlib.LinearAlgebra.Matrix.BilinearForm Mathlib.FieldTheory.PrimitiveElement Mathlib.Geometry.Euclidean.Sphere.Basic Mathlib.RingTheory.RingHom.Integral Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable Mathlib.AlgebraicGeometry.Morphisms.AffineAnd Mathlib.Analysis.Normed.Ring.SeminormFromBounded Mathlib.RingTheory.Smooth.Basic Mathlib.LinearAlgebra.CliffordAlgebra.Even Mathlib.AlgebraicGeometry.AffineSpace Mathlib.LinearAlgebra.Multilinear.FiniteDimensional Mathlib.Combinatorics.Additive.Randomisation Mathlib.NumberTheory.LSeries.Dirichlet Mathlib.RingTheory.Flat.FaithfullyFlat Mathlib.Topology.Algebra.MvPolynomial Mathlib.RingTheory.MvPolynomial.Groebner Mathlib.Analysis.InnerProductSpace.Projection Mathlib.NumberTheory.Fermat Mathlib.NumberTheory.Transcendental.Liouville.Residual Mathlib.MeasureTheory.Integral.Asymptotics Mathlib.Algebra.Polynomial.Degree.CardPowDegree Mathlib.LinearAlgebra.Eigenspace.Triangularizable Mathlib.RingTheory.MvPowerSeries.Inverse Mathlib.Analysis.CStarAlgebra.ApproximateUnit Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog Mathlib.Tactic.NormNum.LegendreSymbol Mathlib.Geometry.Euclidean.Angle.Unoriented.Conformal Mathlib.Analysis.Convex.Strong Mathlib.Analysis.SpecialFunctions.BinaryEntropy Mathlib.LinearAlgebra.Projectivization.Independence Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable Mathlib.LinearAlgebra.Matrix.BaseChange Mathlib.Analysis.Fourier.RiemannLebesgueLemma Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper Mathlib.Analysis.SpecialFunctions.SmoothTransition Mathlib.Data.Complex.FiniteDimensional Mathlib.Analysis.BoxIntegral.Basic Mathlib.RingTheory.Valuation.LocalSubring Mathlib.Analysis.InnerProductSpace.Orthonormal Mathlib.RingTheory.Polynomial.Basic Mathlib.Analysis.Quaternion Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass Mathlib.Analysis.SpecialFunctions.Bernstein Mathlib.Data.Nat.Choose.Factorization Mathlib.Data.Matrix.Kronecker Mathlib.AlgebraicGeometry.FunctionField Mathlib.RingTheory.DedekindDomain.Different Mathlib.AlgebraicGeometry.Morphisms.Constructors Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex Mathlib.Analysis.BoxIntegral.Integrability Mathlib.RingTheory.Discriminant Mathlib.NumberTheory.SumTwoSquares Mathlib.Analysis.InnerProductSpace.Calculus Mathlib.Topology.Category.TopCat.Sphere Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup Mathlib.RingTheory.ReesAlgebra Mathlib.Algebra.Module.PID Mathlib.Algebra.MvPolynomial.Comap Mathlib.NumberTheory.LSeries.Nonvanishing Mathlib.Analysis.Convex.KreinMilman Mathlib.RingTheory.Polynomial.GaussLemma Mathlib.Analysis.Calculus.FDeriv.Norm Mathlib.LinearAlgebra.CliffordAlgebra.Inversion Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp Mathlib.Combinatorics.Additive.AP.Three.Behrend Mathlib.NumberTheory.ClassNumber.Finite Mathlib.FieldTheory.Finiteness Mathlib.Topology.MetricSpace.GromovHausdorff Mathlib.MeasureTheory.Integral.IntegralEqImproper Mathlib.Analysis.Complex.Polynomial.Basic Mathlib.Analysis.Calculus.LocalExtr.Polynomial Mathlib.RingTheory.DedekindDomain.SelmerGroup Mathlib.RingTheory.WittVector.StructurePolynomial Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic Mathlib.NumberTheory.MaricaSchoenheim Mathlib.Analysis.Complex.Tietze Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving Mathlib.LinearAlgebra.Dimension.Torsion.Finite Mathlib.MeasureTheory.Function.L1Space Mathlib.Analysis.NormedSpace.HahnBanach.Extension Mathlib.Probability.Kernel.Disintegration.Basic Mathlib.LinearAlgebra.FreeAlgebra Mathlib.Analysis.Complex.RemovableSingularity Mathlib.RingTheory.DedekindDomain.Basic Mathlib.LinearAlgebra.Matrix.Charpoly.Univ Mathlib.Analysis.Convex.Normed Mathlib.MeasureTheory.Measure.Tilted Mathlib.Analysis.Complex.Liouville Mathlib.RingTheory.AdicCompletion.AsTensorProduct Mathlib.GroupTheory.SpecificGroups.Quaternion Mathlib.NumberTheory.Transcendental.Liouville.Measure Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum Mathlib.Analysis.Convex.Continuous Mathlib.Analysis.InnerProductSpace.LinearMap Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle Mathlib.NumberTheory.LSeries.MellinEqDirichlet Mathlib.AlgebraicGeometry.Morphisms.Smooth Mathlib.Analysis.InnerProductSpace.MeanErgodic Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol Mathlib.RingTheory.Extension Mathlib.Topology.Algebra.Polynomial Mathlib.MeasureTheory.Function.Jacobian Mathlib.FieldTheory.Perfect Mathlib.AlgebraicGeometry.OpenImmersion Mathlib.NumberTheory.DiophantineApproximation.ContinuedFractions Mathlib.NumberTheory.Transcendental.Lindemann.Init.AnalyticalPart Mathlib.Analysis.Complex.LocallyUniformLimit Mathlib.FieldTheory.IsAlgClosed.Basic Mathlib.Algebra.Category.FGModuleCat.Basic Mathlib.NumberTheory.LSeries.Positivity Mathlib.FieldTheory.Minpoly.IsConjRoot Mathlib.Analysis.InnerProductSpace.EuclideanDist Mathlib.RingTheory.DedekindDomain.AdicValuation Mathlib.MeasureTheory.Function.LpOrder Mathlib.RingTheory.DedekindDomain.SInteger Mathlib.Analysis.Convex.Measure Mathlib.Probability.Moments Mathlib.NumberTheory.Harmonic.EulerMascheroni Mathlib.RingTheory.Localization.Free Mathlib.Analysis.SpecialFunctions.Log.Deriv Mathlib.LinearAlgebra.Eigenspace.Basic Mathlib.NumberTheory.LegendreSymbol.AddCharacter Mathlib.FieldTheory.Cardinality Mathlib.Algebra.Lie.EngelSubalgebra Mathlib.NumberTheory.Cyclotomic.PID Mathlib.NumberTheory.JacobiSum.Basic Mathlib.Analysis.Normed.Lp.LpEquiv Mathlib.Topology.MetricSpace.HausdorffDimension Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff Mathlib.Analysis.InnerProductSpace.PiL2 Mathlib.Algebra.Module.CharacterModule Mathlib.AlgebraicGeometry.EllipticCurve.Projective Mathlib.MeasureTheory.Group.FundamentalDomain Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane Mathlib.Algebra.Module.Torsion Mathlib.Analysis.Complex.Conformal Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity Mathlib.Analysis.Normed.Group.AddCircle Mathlib.Topology.Instances.Matrix Mathlib.Topology.Instances.Complex Mathlib.AlgebraicGeometry.AffineScheme Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup Mathlib.RingTheory.RootsOfUnity.Complex Mathlib.Combinatorics.Enumerative.Bell Mathlib.NumberTheory.Padics.RingHoms Mathlib.Topology.ContinuousMap.Weierstrass Mathlib.Analysis.SpecialFunctions.Log.Monotone Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics Mathlib.RingTheory.LocalRing.ResidueField.Basic Mathlib.LinearAlgebra.CliffordAlgebra.Grading Mathlib.Data.Real.Pi.Bounds Mathlib.Data.Nat.Factorization.Root Mathlib.MeasureTheory.Decomposition.Lebesgue Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic Mathlib.Geometry.Manifold.MFDeriv.NormedSpace Mathlib.RingTheory.Polynomial.SeparableDegree Mathlib.RingTheory.KrullDimension.Basic Mathlib.FieldTheory.Separable Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation Mathlib.FieldTheory.MvRatFunc.Rank Mathlib.RingTheory.AlgebraicIndependent.Basic Mathlib.NumberTheory.KummerDedekind Mathlib.AlgebraicGeometry.Limits Mathlib.RingTheory.EisensteinCriterion Mathlib.Geometry.Manifold.MFDeriv.Defs Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional Mathlib.Algebra.Category.Ring.Under.Limits Mathlib.Topology.Algebra.PontryaginDual Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity Mathlib.MeasureTheory.Function.LocallyIntegrable Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence Mathlib.Topology.MetricSpace.Holder Mathlib.Algebra.MvPolynomial.Monad Mathlib.RingTheory.Smooth.StandardSmooth Mathlib.LinearAlgebra.CliffordAlgebra.Basic Mathlib.FieldTheory.IsAlgClosed.Spectrum Mathlib.Topology.Algebra.Valued.ValuationTopology Mathlib.NumberTheory.ModularForms.Basic Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra Mathlib.Analysis.NormedSpace.HahnBanach.Separation Mathlib.Analysis.InnerProductSpace.StarOrder Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated Mathlib.RingTheory.WittVector.Frobenius Mathlib.Analysis.Calculus.LineDeriv.Measurable Mathlib.LinearAlgebra.Vandermonde Mathlib.LinearAlgebra.Matrix.SesquilinearForm Mathlib.RingTheory.Localization.NumDen Mathlib.LinearAlgebra.Projectivization.Cardinality Mathlib.Analysis.NormedSpace.DualNumber Mathlib.NumberTheory.Pell Mathlib.FieldTheory.AlgebraicClosure Mathlib.Probability.Process.Stopping Mathlib.LinearAlgebra.CliffordAlgebra.CategoryTheory Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous Mathlib.RingTheory.IntegralClosure.IntegrallyClosed Mathlib.MeasureTheory.Integral.PeakFunction Mathlib.NumberTheory.NumberField.Basic Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 Mathlib.FieldTheory.CardinalEmb Mathlib.MeasureTheory.Function.SpecialFunctions.Inner Mathlib.Analysis.Normed.Affine.AddTorsorBases Mathlib.NumberTheory.Modular Mathlib.RingTheory.WittVector.Basic Mathlib.NumberTheory.NumberField.Units.DirichletTheorem Mathlib.RingTheory.Jacobson.Ring Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk Mathlib.Tactic.ReduceModChar Mathlib.NumberTheory.ClassNumber.FunctionField Mathlib.MeasureTheory.Integral.MeanInequalities Mathlib.GroupTheory.Transfer Mathlib.RingTheory.Polynomial.Cyclotomic.Expand Mathlib.MeasureTheory.Integral.BoundedContinuousFunction Mathlib.RingTheory.HahnSeries.PowerSeries Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty Mathlib.RepresentationTheory.GroupCohomology.Basic Mathlib.AlgebraicGeometry.PrimeSpectrum.Polynomial Mathlib.RingTheory.Smooth.Kaehler Mathlib.Geometry.Manifold.ContMDiff.Defs Mathlib.Analysis.Normed.Algebra.Basic Mathlib.MeasureTheory.Integral.ExpDecay Mathlib.RepresentationTheory.FDRep Mathlib.AlgebraicGeometry.PrimeSpectrum.Maximal Mathlib.Dynamics.Ergodic.Action.OfMinimal Mathlib.Algebra.MvPolynomial.Equiv Mathlib.RingTheory.WittVector.Isocrystal Mathlib.Geometry.Manifold.IntegralCurve.UniformTime Mathlib.Analysis.SpecialFunctions.Log.Basic Mathlib.NumberTheory.NumberField.Units.Regulator Mathlib.Analysis.Calculus.ContDiff.RCLike Mathlib.Analysis.ODE.Gronwall Mathlib.Analysis.SpecialFunctions.Stirling Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed Mathlib.RingTheory.Trace.Quotient Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality Mathlib.Analysis.LocallyConvex.WeakOperatorTopology Mathlib.SetTheory.Surreal.Multiplication Mathlib.LinearAlgebra.Matrix.Hermitian Mathlib.Analysis.Calculus.Monotone Mathlib.RingTheory.Polynomial.Selmer Mathlib.Analysis.Calculus.Implicit Mathlib.RingTheory.Unramified.Basic Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv Mathlib.FieldTheory.NormalClosure Mathlib.Analysis.SumIntegralComparisons Mathlib.Data.Nat.Factorization.Basic Mathlib.MeasureTheory.VectorMeasure.WithDensity Mathlib.LinearAlgebra.Reflection Mathlib.RingTheory.Adjoin.Dimension Mathlib.LinearAlgebra.AnnihilatingPolynomial Mathlib.RingTheory.Polynomial.UniqueFactorization Mathlib.MeasureTheory.Constructions.HaarToSphere Mathlib.Analysis.SpecialFunctions.JapaneseBracket Mathlib.RingTheory.Valuation.AlgebraInstances Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField Mathlib.MeasureTheory.Integral.CircleTransform Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent Mathlib.NumberTheory.FermatPsp Mathlib.RingTheory.Kaehler.Basic Mathlib.GroupTheory.Sylow Mathlib.MeasureTheory.Integral.DominatedConvergence Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField Mathlib.NumberTheory.VonMangoldt Mathlib.NumberTheory.ZetaValues Mathlib.Analysis.Convex.Deriv Mathlib.NumberTheory.Cyclotomic.Basic Mathlib.RingTheory.MvPowerSeries.Order Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine Mathlib.Topology.MetricSpace.HolderNorm Mathlib.Analysis.SpecialFunctions.Arsinh Mathlib.Analysis.Complex.Positivity Mathlib.Analysis.Calculus.ContDiff.FiniteDimension Mathlib.RingTheory.MvPolynomial.MonomialOrder Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure Mathlib.MeasureTheory.Function.ConvergenceInMeasure Mathlib.Analysis.Fourier.FourierTransform Mathlib.LinearAlgebra.Dimension.LinearMap Mathlib.LinearAlgebra.Matrix.LDL Mathlib.Tactic.FunProp.Differentiable Mathlib.Probability.Independence.Integrable Mathlib.RingTheory.AdjoinRoot Mathlib.Geometry.Manifold.MFDeriv.Tangent Mathlib.Algebra.Lie.Weights.Killing Mathlib.Analysis.Matrix Mathlib.Analysis.Convex.Uniform Mathlib.AlgebraicGeometry.Morphisms.FiniteType Mathlib.LinearAlgebra.Matrix.ProjectiveSpecialLinearGroup Mathlib.Analysis.SpecialFunctions.Pow.Real Mathlib.RingTheory.Valuation.ValuationSubring Mathlib.RingTheory.Smooth.Pi Mathlib.RingTheory.LocalProperties.IntegrallyClosed Mathlib.Algebra.MvPolynomial.Cardinal Mathlib.Algebra.MvPolynomial.Division Mathlib.Probability.IdentDistrib Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances Mathlib.RingTheory.Complex Mathlib.Dynamics.TopologicalEntropy.Semiconj Mathlib.Topology.ContinuousMap.StoneWeierstrass Mathlib.Analysis.Convolution Mathlib.AlgebraicGeometry.Scheme Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle Mathlib.LinearAlgebra.Matrix.Adjugate Mathlib.LinearAlgebra.Matrix.SchurComplement Mathlib.RingTheory.Etale.Pi Mathlib.RingTheory.Flat.EquationalCriterion Mathlib.LinearAlgebra.Eigenspace.Semisimple Mathlib.Analysis.Calculus.Conformal.InnerProduct Mathlib.Analysis.Calculus.VectorField Mathlib.FieldTheory.KummerExtension Mathlib.NumberTheory.LucasPrimality Mathlib.Algebra.Algebra.Subalgebra.IsSimpleOrder Mathlib.RingTheory.Polynomial.Cyclotomic.Eval Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp Mathlib.AlgebraicGeometry.Gluing Mathlib.LinearAlgebra.QuadraticForm.Isometry Mathlib.RingTheory.Jacobson.Polynomial Mathlib.Topology.Instances.Irrational Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty Mathlib.ModelTheory.Algebra.Ring.FreeCommRing Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition Mathlib.Analysis.Complex.Arg Mathlib.Geometry.Manifold.Algebra.Monoid Mathlib.FieldTheory.Minpoly.Field Mathlib.LinearAlgebra.UnitaryGroup Mathlib.Topology.Algebra.Module.Determinant Mathlib.SetTheory.Cardinal.Free Mathlib.Topology.MetricSpace.Kuratowski Mathlib.Algebra.Module.LinearMap.Polynomial Mathlib.Analysis.MellinInversion Mathlib.NumberTheory.BernoulliPolynomials Mathlib.RepresentationTheory.GroupCohomology.LowDegree Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear Mathlib.LinearAlgebra.BilinearForm.TensorProduct Mathlib.AlgebraicGeometry.Cover.Open Mathlib.Analysis.Convex.Cone.InnerDual Mathlib.Geometry.Manifold.Algebra.Structures Mathlib.AlgebraicGeometry.Stalk Mathlib.RingTheory.AdicCompletion.Algebra Mathlib.Algebra.FreeAlgebra.Cardinality Mathlib.RingTheory.Polynomial.Eisenstein.Basic Mathlib.Analysis.CStarAlgebra.Hom Mathlib.Analysis.Complex.Polynomial.UnitTrinomial Mathlib.Geometry.Manifold.PartitionOfUnity Mathlib.LinearAlgebra.Dimension.Free Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian Mathlib.NumberTheory.PrimeCounting Mathlib.LinearAlgebra.Dual Mathlib.Analysis.Complex.UpperHalfPlane.Basic Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv Mathlib.Geometry.Manifold.MFDeriv.Atlas Mathlib.MeasureTheory.Measure.SeparableMeasure Mathlib.Analysis.Normed.Ring.IsPowMulFaithful Mathlib.NumberTheory.Padics.Hensel Mathlib.MeasureTheory.Covering.Differentiation Mathlib.Data.Nat.Choose.Multinomial Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange Mathlib.GroupTheory.FiniteAbelian.Duality Mathlib.NumberTheory.LSeries.HurwitzZetaOdd Mathlib.RingTheory.FractionalIdeal.Operations Mathlib.LinearAlgebra.QuadraticForm.TensorProduct Mathlib.Data.Finsupp.MonomialOrder.DegLex Mathlib.ModelTheory.Algebra.Field.IsAlgClosed Mathlib.Analysis.Complex.Hadamard Mathlib.RingTheory.Etale.Basic Mathlib.RingTheory.LinearDisjoint Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap Mathlib.Geometry.Manifold.Algebra.LieGroup Mathlib.FieldTheory.JacobsonNoether Mathlib.NumberTheory.PrimesCongruentOne Mathlib.LinearAlgebra.Dimension.Torsion.Basic Mathlib.Combinatorics.SimpleGraph.LapMatrix Mathlib.ModelTheory.Algebra.Field.CharP Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange Mathlib.Analysis.BoundedVariation Mathlib.Analysis.InnerProductSpace.Adjoint Mathlib.Analysis.InnerProductSpace.Semisimple Mathlib.Combinatorics.SimpleGraph.Regularity.Bound Mathlib.RingTheory.WittVector.Teichmuller Mathlib.NumberTheory.WellApproximable Mathlib.RingTheory.LocalRing.Module Mathlib.MeasureTheory.Measure.Lebesgue.Basic Mathlib.LinearAlgebra.CliffordAlgebra.Contraction Mathlib.NumberTheory.LSeries.Convergence Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order Mathlib.NumberTheory.Transcendental.Liouville.Basic Mathlib.Probability.Process.Adapted Mathlib.Analysis.Convex.Cone.Proper Mathlib.RingTheory.MvPolynomial.Basic Mathlib.Algebra.MvPolynomial.PDeriv Mathlib.Probability.Distributions.Pareto Mathlib.NumberTheory.DirichletCharacter.Bounds Mathlib.Algebra.Lie.Sl2 Mathlib.Analysis.Convex.Cone.Closure Mathlib.MeasureTheory.Measure.Lebesgue.Integral Mathlib.RingTheory.FreeCommRing Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality Mathlib.RingTheory.PowerSeries.Order Mathlib.FieldTheory.PurelyInseparable Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv Mathlib.Analysis.Calculus.Gradient.Basic Mathlib.Algebra.MvPolynomial.CommRing Mathlib.Algebra.Polynomial.Module.FiniteDimensional Mathlib.Analysis.Calculus.Rademacher Mathlib.Analysis.Convex.Visible Mathlib.Analysis.Calculus.BumpFunction.InnerProduct Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace Mathlib.LinearAlgebra.Matrix.Spectrum Mathlib.RingTheory.WittVector.IsPoly Mathlib.RingTheory.Kaehler.TensorProduct Mathlib.LinearAlgebra.Dimension.Constructions Mathlib.MeasureTheory.Integral.Pi Mathlib.NumberTheory.NumberField.House Mathlib.LinearAlgebra.Dimension.ErdosKaplansky Mathlib.Analysis.Normed.Module.Complemented Mathlib.Analysis.InnerProductSpace.l2Space Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap Mathlib.GroupTheory.SpecificGroups.Cyclic Mathlib.Analysis.Complex.UpperHalfPlane.Exp Mathlib.NumberTheory.NumberField.Embeddings Mathlib.MeasureTheory.Function.Intersectivity Mathlib.Dynamics.TopologicalEntropy.CoverEntropy Mathlib.Analysis.CStarAlgebra.lpSpace Mathlib.Algebra.Lie.Weights.Cartan Mathlib.Probability.Process.Filtration Mathlib.AlgebraicGeometry.GammaSpecAdjunction Mathlib.MeasureTheory.Integral.Periodic Mathlib.RingTheory.Valuation.Minpoly Mathlib.NumberTheory.Harmonic.Bounds Mathlib.RingTheory.Artinian.Instances Mathlib.NumberTheory.Bernoulli Mathlib.LinearAlgebra.SymplecticGroup Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ Mathlib.Geometry.Manifold.AnalyticManifold Mathlib.Analysis.MellinTransform Mathlib.LinearAlgebra.Determinant Mathlib.RingTheory.Flat.Equalizer Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating Mathlib.Analysis.Convex.StrictConvexBetween Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar Mathlib.NumberTheory.LSeries.Linearity Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card Mathlib.MeasureTheory.Integral.Gamma Mathlib.Geometry.Manifold.ContMDiff.NormedSpace Mathlib.Analysis.VonNeumannAlgebra.Basic Mathlib.MeasureTheory.Measure.DiracProba Mathlib.MeasureTheory.Integral.IntegrableOn Mathlib.Topology.Algebra.Valued.ValuedField Mathlib.Analysis.Convex.SpecificFunctions.Deriv Mathlib.Analysis.Normed.Module.WeakDual Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd Mathlib.MeasureTheory.Integral.SetToL1 Mathlib.Algebra.Lie.Engel Mathlib.Analysis.Calculus.FDeriv.Symmetric Mathlib.RingTheory.WittVector.Defs Mathlib.Algebra.Category.ModuleCat.Free Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear Mathlib.RingTheory.FiniteLength Mathlib.Algebra.MvPolynomial.Polynomial Mathlib.Geometry.Euclidean.Inversion.Basic Mathlib.Algebra.Lie.Rank Mathlib.Probability.Kernel.Condexp Mathlib.Topology.Algebra.Valued.LocallyCompact Mathlib.GroupTheory.FiniteAbelian.Basic Mathlib.RingTheory.IntegralClosure.Algebra.Basic Mathlib.AlgebraicGeometry.Cover.MorphismProperty Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks Mathlib.LinearAlgebra.AffineSpace.Matrix Mathlib.GroupTheory.Order.Min Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv Mathlib.FieldTheory.PerfectClosure Mathlib.LinearAlgebra.CliffordAlgebra.Prod Mathlib.AlgebraicGeometry.GluingOneHypercover Mathlib.LinearAlgebra.Eigenspace.Pi Mathlib.FieldTheory.Galois.Infinite Mathlib.Algebra.Lie.Classical Mathlib.RingTheory.MvPowerSeries.Trunc Mathlib.NumberTheory.LSeries.PrimesInAP Mathlib.Analysis.SpecialFunctions.Complex.Circle Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries Mathlib.Algebra.Polynomial.Bivariate Mathlib.RingTheory.DedekindDomain.Factorization Mathlib.AlgebraicGeometry.ValuativeCriterion Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma Mathlib.Geometry.Euclidean.Triangle Mathlib.AlgebraicGeometry.Restrict Mathlib.AlgebraicGeometry.PullbackCarrier Mathlib.MeasureTheory.Covering.Besicovitch Mathlib.RingTheory.MvPowerSeries.Basic Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension Mathlib.Analysis.Complex.IntegerCompl Mathlib.GroupTheory.SpecificGroups.KleinFour Mathlib.Probability.Distributions.Gamma Mathlib.LinearAlgebra.Eigenspace.Zero Mathlib.Probability.Martingale.OptionalStopping Mathlib.RingTheory.Flat.Stability Mathlib.Probability.Martingale.BorelCantelli Mathlib.Analysis.SpecialFunctions.ExpDeriv Mathlib.RingTheory.FiniteType Mathlib.Geometry.Manifold.DerivationBundle Mathlib.LinearAlgebra.Eigenspace.Minpoly Mathlib.NumberTheory.Padics.ProperSpace Mathlib.Probability.Density Mathlib.Data.Nat.Factorization.PrimePow Mathlib.LinearAlgebra.Projectivization.Subspace Mathlib.Analysis.Complex.OpenMapping Mathlib.AlgebraicGeometry.PrimeSpectrum.IsOpenComapC Mathlib.Probability.ProbabilityMassFunction.Integrals Mathlib.Data.Complex.Orientation Mathlib.RingTheory.Polynomial.RationalRoot Mathlib.RingTheory.WittVector.FrobeniusFractionField Mathlib.LinearAlgebra.Matrix.ToLinearEquiv Mathlib.Analysis.Calculus.BumpFunction.Normed Mathlib.Analysis.NormedSpace.Connected Mathlib.Algebra.MvPolynomial.Degrees Mathlib.RingTheory.IntegralDomain Mathlib.Geometry.Manifold.IntegralCurve.Transform Mathlib.Analysis.ODE.PicardLindelof Mathlib.GroupTheory.SpecificGroups.Dihedral Mathlib.RingTheory.RootsOfUnity.Minpoly Mathlib.NumberTheory.NumberField.ClassNumber Mathlib.Probability.ConditionalExpectation Mathlib.MeasureTheory.Integral.SetIntegral Mathlib.Analysis.Analytic.Polynomial Mathlib.Analysis.InnerProductSpace.ConformalLinearMap Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv Mathlib.Algebra.CharP.MixedCharZero Mathlib.GroupTheory.Frattini Mathlib.RingTheory.WittVector.DiscreteValuationRing Mathlib.Geometry.Manifold.LocalDiffeomorph Mathlib.RingTheory.MvPowerSeries.PiTopology Mathlib.FieldTheory.PolynomialGaloisGroup Mathlib.Analysis.InnerProductSpace.Orientation Mathlib.Geometry.Euclidean.Angle.Oriented.Affine Mathlib.Algebra.MvPolynomial.Invertible Mathlib.GroupTheory.PGroup Mathlib.NumberTheory.ModularForms.CongruenceSubgroups Mathlib.LinearAlgebra.Dimension.Finite Mathlib.RingTheory.DedekindDomain.PID Mathlib.Analysis.SpecialFunctions.Pow.NNReal Mathlib.Algebra.Category.Grp.Injective Mathlib.FieldTheory.AxGrothendieck Mathlib.LinearAlgebra.RootSystem.RootPositive Mathlib.NumberTheory.LSeries.HurwitzZeta Mathlib.Tactic Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform Mathlib.MeasureTheory.Function.LpSpace.DomAct.Continuous Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed Mathlib.Geometry.Euclidean.PerpBisector Mathlib.NumberTheory.NumberField.FinitePlaces Mathlib.Analysis.Convex.SpecificFunctions.Basic Mathlib.MeasureTheory.Group.Integral Mathlib.LinearAlgebra.Matrix.IsDiag Mathlib.Analysis.Convex.Radon Mathlib.Algebra.Category.Ring.Adjunctions Mathlib.RingTheory.Norm.Transitivity Mathlib.FieldTheory.SplittingField.Construction Mathlib.FieldTheory.RatFunc.Basic Mathlib.MeasureTheory.Measure.Haar.Disintegration Mathlib.LinearAlgebra.Charpoly.BaseChange Mathlib.Algebra.Lie.Weights.Linear Mathlib.RingTheory.Unramified.Finite Mathlib.RepresentationTheory.Maschke Mathlib.RingTheory.Kaehler.JacobiZariski Mathlib.Probability.Integration Mathlib.Analysis.Distribution.SchwartzSpace Mathlib.NumberTheory.Bertrand Mathlib.GroupTheory.Schreier Mathlib.RingTheory.NormTrace Mathlib.RingTheory.Derivation.MapCoeffs Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber Mathlib.LinearAlgebra.RootSystem.Hom Mathlib.Combinatorics.Additive.CauchyDavenport Mathlib.Analysis.SpecialFunctions.Gamma.Deriv Mathlib.Geometry.Manifold.Metrizable Mathlib.Analysis.BoxIntegral.DivergenceTheorem Mathlib.NumberTheory.LSeries.Convolution Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral Mathlib.LinearAlgebra.Dimension.RankNullity Mathlib.LinearAlgebra.Basis.Flag Mathlib.LinearAlgebra.Matrix.NonsingularInverse Mathlib.Algebra.Polynomial.Cardinal Mathlib.Algebra.Lie.InvariantForm Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic Mathlib.Analysis.SpecialFunctions.Pow.Integral Mathlib.Geometry.Manifold.WhitneyEmbedding Mathlib.FieldTheory.RatFunc.Degree Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis Mathlib.RingTheory.RootsOfUnity.Basic Mathlib.Algebra.Lie.CartanExists Mathlib.RingTheory.Localization.Away.AdjoinRoot Mathlib.NumberTheory.FLT.MasonStothers Mathlib.Probability.Kernel.Integral Mathlib.MeasureTheory.Integral.Average Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed Mathlib.Probability.Kernel.Disintegration.Unique Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus Mathlib.Probability.Independence.Conditional Mathlib.NumberTheory.AbelSummation Mathlib.RingTheory.PowerSeries.Trunc Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic Mathlib.MeasureTheory.Function.ConditionalExpectation.Real Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog Mathlib.LinearAlgebra.Matrix.FixedDetMatrices Mathlib.RingTheory.Perfection Mathlib.RingTheory.Norm.Basic Mathlib.Data.Real.Pi.Wallis Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt Mathlib.Probability.Process.PartitionFiltration Mathlib.Probability.Notation Mathlib.NumberTheory.LSeries.AbstractFuncEq Mathlib.NumberTheory.FunctionField Mathlib.Algebra.DirectSum.LinearMap Mathlib.Probability.CDF Mathlib.LinearAlgebra.ExteriorAlgebra.Basic Mathlib.Data.Nat.Totient Mathlib.RingTheory.PowerSeries.Basic Mathlib.RingTheory.TensorProduct.MvPolynomial Mathlib.NumberTheory.EulerProduct.ExpLog Mathlib.NumberTheory.FLT.Polynomial Mathlib.RingTheory.AlgebraicIndependent.Adjoin Mathlib.LinearAlgebra.Matrix.Dual Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors Mathlib.GroupTheory.SpecificGroups.ZGroup Mathlib.RingTheory.LocalProperties.Projective Mathlib.MeasureTheory.Measure.Haar.OfBasis Mathlib.Data.Complex.ExponentialBounds Mathlib.Analysis.InnerProductSpace.TwoDim Mathlib.NumberTheory.NumberField.AdeleRing Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic Mathlib.Probability.Martingale.Centering Mathlib.Algebra.Colimit.Ring Mathlib.RingTheory.PowerSeries.Inverse Mathlib.Analysis.Calculus.ContDiff.WithLp Mathlib.LinearAlgebra.QuadraticForm.Dual Mathlib.AlgebraicGeometry.Morphisms.Etale Mathlib.NumberTheory.ModularForms.QExpansion Mathlib.MeasureTheory.Measure.Haar.Quotient Mathlib.Topology.Instances.RatLemmas Mathlib.Geometry.Manifold.Instances.Sphere Mathlib.NumberTheory.DiophantineApproximation.Basic Mathlib.LinearAlgebra.Matrix.Block Mathlib.Geometry.Manifold.VectorBundle.SmoothSection Mathlib.Geometry.Manifold.ContMDiff.Product Mathlib.LinearAlgebra.RootSystem.Defs Mathlib.Analysis.InnerProductSpace.LaxMilgram Mathlib.LinearAlgebra.Projectivization.Basic Mathlib.RingTheory.WittVector.MulP Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate Mathlib.Analysis.Normed.Algebra.UnitizationL1 Mathlib.Data.Nat.Factorial.SuperFactorial
 1
Mathlib.Data.Multiset.Sum Mathlib.Data.PNat.Factors 2
4 files Mathlib.Algebra.Order.BigOperators.Ring.Multiset Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset Mathlib.Data.Sym.Basic Mathlib.Algebra.BigOperators.Group.Multiset
 3
Mathlib.Data.Multiset.OrderedMonoid Mathlib.Algebra.Order.Group.Multiset 5

Declarations diff

+ Nodup.le_nsmul_iff_le
+ toFinset_card_eq_one_iff
- Multiset.Nodup.le_nsmul_iff_le
- _root_.Multiset.toFinset_card_eq_one_iff

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 mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Dec 7, 2024
@YaelDillies YaelDillies changed the base branch from multiset_no_algebra to master December 7, 2024 14:16
Vierkantor
Vierkantor reviewed Dec 9, 2024
View reviewed changes
Copy link
Contributor

@Vierkantor Vierkantor left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So here we end up defining much of the OrderedAddCommMonoid structure anyway, except as separate lemmas rather than instances of that class. I'll have to think for a moment if that really is simple enough to be worth the effort.

@YaelDillies
Copy link
Collaborator Author

Indeed that's basically what's happening, and this is the reason why I didn't do this import reduction months ago when I was reducing many imports in basic algebra and basic order theory. The reason I now think this is worth doing is that saying "Don't import Monoid" is a very clear and simple ask (rather than "don't import these 10 files that currently happen to form a cut of the algebra library") which we could implement in all the basic finiteness library as well as basic topology.

@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 9, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 9, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 18, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 23, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 6, 2025
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Jan 7, 2025
@mathlib4-dependent-issues-bot
Copy link
Collaborator

This PR/issue depends on:

@YaelDillies YaelDillies requested a review from Vierkantor January 7, 2025 08:01
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 7, 2025
@Vierkantor
Copy link
Contributor

I see that I had already reviewed and approved almost all the files last month. And indeed "don't import Monoid" is a very good measure, so let's get this merged!

bors r+

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the ready-to-merge This PR has been sent to bors. label Jan 7, 2025
mathlib-bors bot pushed a commit that referenced this pull request Jan 7, 2025
@YaelDillies
chore: don't import algebra in Data.Finset.Basic (#19779)
7d091da
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jan 7, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: don't import algebra in Data.Finset.Basic [Merged by Bors] - chore: don't import algebra in Data.Finset.Basic Jan 7, 2025
@mathlib-bors mathlib-bors bot closed this Jan 7, 2025
@mathlib-bors mathlib-bors bot deleted the finset_no_algebra branch January 7, 2025 10:02
Julian added a commit that referenced this pull request Jan 8, 2025
@Julian
Merge remote-tracking branch 'origin/master' into emultiplicity-of-nat
53d4c08 
* origin/master: (642 commits)
  feat: the Boolean subalgebra generated by the lattice generated by a set (#20440)
  feat: misc. lemmas about moments, tilted measures (#20150)
  chore(Algebra/Lie): make IsNilpotent and IsSolvable independent of scalars (#20556)
  feat(Combinatorics/SimpleGraph/Path): add `IsPath.getVert_injOn` (#19373)
  feat(Combinatorics/SimpleGraph): add lemmas about `spanningCoe` (#19377)
  chore: scope 'on' notation to Function (#20562)
  chore: disable docPrime linter (#20559)
  chore: deprecate MulRingNorm._ in favour of AbsoluteValue._ (#20557)
  fix(scripts/bench_summary): input jobID as a Nat, rather than a String (#20539)
  chore: move results about `DivisionMonoid` + `HasDistribNeg` (#20551)
  feat(NumberTheory/NumberField/Embeddings): definition of totally real field (#20542)
  chore(Noetherian/Artinian): generalize to Semiring (#20534)
  chore: protect `Filter.nhds_{iInf,inf}` (#20530)
  chore(AlgebraicTopology): move SplitSimplicialObject.lean (#20511)
  chore: extract 3 new files out of MeasureSpace (#20509)
  feat(RingTheory): Jacobian criterion for smoothness of local algebras (#20326)
  doc(RingTheory/Flat): add reference to Lambek's paper (#20266)
  feat(NumberTheory/AbelSummation): add more results (#19942)
  chore(Multilinear/Basic): generalize the `SMul` instance (#20536)
  feat(FDeriv/Equiv): generalize `HasFDerivAt.of_local_left_inverse` (#20516)
  feat(ContDiff): add `iteratedFDeriv_comp` (#20472)
  feat(LowerUpperTopology): add lemmas (#20465)
  feat(ContDiff): weaken some assumptions (#20368)
  fix(scripts/technical-debt-metric): avoid division by 0 (#20537)
  chore(Algebra/Ring): Clean up in SumsOfSquares and Semireal/Defs (#20528)
  feat(FTaylorSeries): add lemmas about `dist` between 0th and 1st derivs (#20089)
  feat: results on inner regularity of finite measures (#19780)
  chore: to_additive various results on groups, group actions (#20547)
  feat(Probability/Kernel): `Kernel.sectL` and `sectR` (#15466)
  chore(CategoryTheory/Limits/Fubini): relax universes constraints and weaken hypotheses (#20553)
  perf: remove `@[simp]` on `Fintype.card_of{IsEmpty,Subsingleton}` (#20524)
  fix(HashCommandLinter): remove unnecessary, broken workaround for tests (#20529)
  chore(Ideal/Basic): dependent generalization of `Ideal.pi` (#20535)
  feat(RingTheory): being unramified is a local property (#20323)
  chore(BooleanSubalgebra): use `IsSublattice` in `closure_sdiff_sup_induction` (#20439)
  feat(Order/SuccPred/CompleteLinearOrder): `⨆ a < x, succ a = x` (#19970)
  chore(*): replace `no_index (ofNat n)` with `ofNat(n)` everywhere (#20521)
  feat(CategoryTheory/Triangulated/Adjunction): the right adjoint of a triangulated functor is triangulated (#20255)
  chore(Order/SuccPred/LinearLocallyFinite): change data-creating instances to defs (#20235)
  chore: don't import algebra in `Data.Finset.Basic` (#19779)
  feat: initial segment commutes with `Iio` (#20503)
  chore(Measure/Pi): move parts to `MeasurableSpace/` (#20215)
  chore: smile more often (#20436)
  chore(Algebra/Category/MonCat/ForgetCorepresentable, Algebra/Group/Equiv/Basic): move definitions and add symmetric version (#20416)
  feat(GroupTheory/QuotientGroup): group correspondence theorem (#20007)
  doc: change "module homomorphism" to "linear map" (#20481)
  perf: improves the performance of the `Repr (Equiv.Perm α)` instance (1/4) (#20519)
  fix: do not keep only the first line of hints (#19756)
  feat(Analysis/Analytic): lemmas about `smul` for power series (#19816)
  chore: don't import algebra in `Data.Multiset.Basic` (#19775)
  ...
Julian added a commit that referenced this pull request Jan 8, 2025
@Julian
Merge remote-tracking branch 'origin/master' into bhargava-factorial
0ae6406 
* origin/master: (80 commits)
  chore(CategoryTheory): remove data produced by tactic block (#20565)
  feat: `|∫ a, f a ∂μ| ≤ ∫ a, |f a| ∂μ` (#20540)
  feat: the Boolean subalgebra generated by the lattice generated by a set (#20440)
  feat: misc. lemmas about moments, tilted measures (#20150)
  chore(Algebra/Lie): make IsNilpotent and IsSolvable independent of scalars (#20556)
  feat(Combinatorics/SimpleGraph/Path): add `IsPath.getVert_injOn` (#19373)
  feat(Combinatorics/SimpleGraph): add lemmas about `spanningCoe` (#19377)
  chore: scope 'on' notation to Function (#20562)
  chore: disable docPrime linter (#20559)
  chore: deprecate MulRingNorm._ in favour of AbsoluteValue._ (#20557)
  fix(scripts/bench_summary): input jobID as a Nat, rather than a String (#20539)
  chore: move results about `DivisionMonoid` + `HasDistribNeg` (#20551)
  feat(NumberTheory/NumberField/Embeddings): definition of totally real field (#20542)
  chore(Noetherian/Artinian): generalize to Semiring (#20534)
  chore: protect `Filter.nhds_{iInf,inf}` (#20530)
  chore(AlgebraicTopology): move SplitSimplicialObject.lean (#20511)
  chore: extract 3 new files out of MeasureSpace (#20509)
  feat(RingTheory): Jacobian criterion for smoothness of local algebras (#20326)
  doc(RingTheory/Flat): add reference to Lambek's paper (#20266)
  feat(NumberTheory/AbelSummation): add more results (#19942)
  chore(Multilinear/Basic): generalize the `SMul` instance (#20536)
  feat(FDeriv/Equiv): generalize `HasFDerivAt.of_local_left_inverse` (#20516)
  feat(ContDiff): add `iteratedFDeriv_comp` (#20472)
  feat(LowerUpperTopology): add lemmas (#20465)
  feat(ContDiff): weaken some assumptions (#20368)
  fix(scripts/technical-debt-metric): avoid division by 0 (#20537)
  chore(Algebra/Ring): Clean up in SumsOfSquares and Semireal/Defs (#20528)
  feat(FTaylorSeries): add lemmas about `dist` between 0th and 1st derivs (#20089)
  feat: results on inner regularity of finite measures (#19780)
  chore: to_additive various results on groups, group actions (#20547)
  feat(Probability/Kernel): `Kernel.sectL` and `sectR` (#15466)
  chore(CategoryTheory/Limits/Fubini): relax universes constraints and weaken hypotheses (#20553)
  perf: remove `@[simp]` on `Fintype.card_of{IsEmpty,Subsingleton}` (#20524)
  fix(HashCommandLinter): remove unnecessary, broken workaround for tests (#20529)
  chore(Ideal/Basic): dependent generalization of `Ideal.pi` (#20535)
  feat(RingTheory): being unramified is a local property (#20323)
  chore(BooleanSubalgebra): use `IsSublattice` in `closure_sdiff_sup_induction` (#20439)
  feat(Order/SuccPred/CompleteLinearOrder): `⨆ a < x, succ a = x` (#19970)
  chore(*): replace `no_index (ofNat n)` with `ofNat(n)` everywhere (#20521)
  feat(CategoryTheory/Triangulated/Adjunction): the right adjoint of a triangulated functor is triangulated (#20255)
  chore(Order/SuccPred/LinearLocallyFinite): change data-creating instances to defs (#20235)
  chore: don't import algebra in `Data.Finset.Basic` (#19779)
  feat: initial segment commutes with `Iio` (#20503)
  chore(Measure/Pi): move parts to `MeasurableSpace/` (#20215)
  chore: smile more often (#20436)
  chore(Algebra/Category/MonCat/ForgetCorepresentable, Algebra/Group/Equiv/Basic): move definitions and add symmetric version (#20416)
  feat(GroupTheory/QuotientGroup): group correspondence theorem (#20007)
  doc: change "module homomorphism" to "linear map" (#20481)
  perf: improves the performance of the `Repr (Equiv.Perm α)` instance (1/4) (#20519)
  fix: do not keep only the first line of hints (#19756)
  ...
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Vierkantor Vierkantor Awaiting requested review from Vierkantor

Assignees
No one assigned
Labels
ready-to-merge This PR has been sent to bors. t-data Data (lists, quotients, numbers, etc)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
5 participants
@YaelDillies @mathlib4-dependent-issues-bot @Vierkantor @leanprover-community-bot-assistant @leanprover-community-mathlib4-bot