Skip to content

[Merged by Bors] - perf: improves the performance of the Repr (Equiv.Perm α) instance (1/4)#20519

Closed
Komyyy wants to merge 2 commits intomasterfrom
Komyyy/Equiv.Perm.instRepr3
Closed

[Merged by Bors] - perf: improves the performance of the Repr (Equiv.Perm α) instance (1/4)#20519
Komyyy wants to merge 2 commits intomasterfrom
Komyyy/Equiv.Perm.instRepr3

Conversation

@Komyyy
Copy link
Copy Markdown
Contributor

@Komyyy Komyyy commented Jan 6, 2025 •
edited
Loading

This PR reduces computation time from $O(n^2)$ (more precisery, $O(\sum_{k<n} k)$.) to $O(n)$ by using List.iterate.

Open in Gitpod

@Komyyy Komyyy added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-algebra Algebra (groups, rings, fields, etc) labels Jan 6, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jan 6, 2025 •
edited
Loading

PR summary e349bf735d

Import changes for modified files

Dependency changes

File Base Count Head Count Change
Mathlib.GroupTheory.Perm.Cycle.Basic 882 883 +1 (+0.11%)
Mathlib.GroupTheory.Perm.Cycle.Factors 883 884 +1 (+0.11%)
Mathlib.GroupTheory.Perm.Cycle.Concrete 908 909 +1 (+0.11%)
Import changes for all files
Files Import difference
971 files Mathlib.LinearAlgebra.FreeModule.Norm Mathlib.LinearAlgebra.Charpoly.Basic Mathlib.NumberTheory.NumberField.Discriminant.Defs Mathlib.MeasureTheory.Integral.VitaliCaratheodory Mathlib.RingTheory.FractionalIdeal.Norm 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.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Symmetric Mathlib.FieldTheory.IsPerfectClosure Mathlib.Probability.BorelCantelli Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv Mathlib.NumberTheory.Wilson Mathlib.Geometry.Manifold.ContMDiff.Atlas Mathlib.RepresentationTheory.GroupCohomology.Hilbert90 Mathlib.NumberTheory.LSeries.HurwitzZetaValues Mathlib.RingTheory.PowerBasis Mathlib.Analysis.SpecialFunctions.Gamma.Basic Mathlib.Geometry.Manifold.VectorBundle.Pullback Mathlib.FieldTheory.Finite.Trace 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.Analysis.SpecialFunctions.Integrals Mathlib.NumberTheory.Harmonic.ZetaAsymp Mathlib.Dynamics.Ergodic.AddCircle Mathlib.Analysis.Calculus.BumpFunction.Convolution 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.NumberTheory.Cyclotomic.Discriminant Mathlib.AlgebraicGeometry.Morphisms.Preimmersion Mathlib.GroupTheory.Perm.Cycle.PossibleTypes Mathlib.Geometry.Manifold.VectorBundle.Basic Mathlib.Analysis.Calculus.Deriv.Abs Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds Mathlib.MeasureTheory.Measure.FiniteMeasure Mathlib.Tactic.FunProp.ContDiff Mathlib.AlgebraicGeometry.PrimeSpectrum.TensorProduct 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.Data.Matrix.DoublyStochastic Mathlib.NumberTheory.GaussSum Mathlib.Analysis.Convex.Birkhoff Mathlib.Geometry.Manifold.Diffeomorph Mathlib.Combinatorics.Additive.Corner.Roth Mathlib.MeasureTheory.Measure.Lebesgue.Complex Mathlib.NumberTheory.EulerProduct.DirichletLSeries Mathlib.RingTheory.DedekindDomain.Ideal Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology Mathlib.MeasureTheory.Integral.IntervalIntegral Mathlib.Analysis.Calculus.FDeriv.WithLp Mathlib.AlgebraicGeometry.Sites.MorphismProperty Mathlib.Analysis.Complex.AbsMax Mathlib.AlgebraicGeometry.Sites.BigZariski Mathlib.RingTheory.Ideal.Over Mathlib.Analysis.InnerProductSpace.ProdL2 Mathlib.Probability.Kernel.Disintegration.CDFToKernel Mathlib.RingTheory.LocalRing.Quotient Mathlib.Algebra.Category.ModuleCat.Differentials.Basic Mathlib.RingTheory.WittVector.InitTail Mathlib.Geometry.Manifold.MFDeriv.Basic Mathlib.Analysis.CStarAlgebra.Spectrum Mathlib.Geometry.Manifold.Instances.Real Mathlib.RingTheory.Localization.NormTrace Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv Mathlib.LinearAlgebra.Lagrange Mathlib.Geometry.Manifold.Complex Mathlib.FieldTheory.AbelRuffini Mathlib.RingTheory.ClassGroup Mathlib.AlgebraicGeometry.Morphisms.Basic Mathlib.NumberTheory.LSeries.DirichletContinuation Mathlib.MeasureTheory.Integral.CircleIntegral Mathlib.Probability.StrongLaw Mathlib.RingTheory.Regular.RegularSequence Mathlib.Analysis.Normed.Module.FiniteDimension Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique Mathlib.NumberTheory.NumberField.FractionalIdeal Mathlib.AlgebraicGeometry.Morphisms.IsIso Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral Mathlib.AlgebraicGeometry.Modules.Presheaf Mathlib.Probability.Kernel.Composition.MeasureCompProd Mathlib.Algebra.Module.DedekindDomain Mathlib.RingTheory.Trace.Defs Mathlib.RingTheory.WittVector.Compare Mathlib.GroupTheory.Perm.Cycle.Basic Mathlib.Probability.Kernel.Composition.IntegralCompProd Mathlib.Analysis.SpecialFunctions.Gamma.Beta Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure Mathlib.MeasureTheory.Integral.TorusIntegral Mathlib.Analysis.Complex.Isometry Mathlib.RingTheory.Adjoin.PowerBasis Mathlib.Geometry.Manifold.MFDeriv.FDeriv Mathlib.Analysis.Convex.Side Mathlib.MeasureTheory.Function.L2Space Mathlib.AlgebraicGeometry.PrimeSpectrum.FreeLocus Mathlib.MeasureTheory.Measure.LevyProkhorovMetric Mathlib.Algebra.Module.ZLattice.Covolume Mathlib.RingTheory.AdicCompletion.Functoriality Mathlib.LinearAlgebra.PID Mathlib.LinearAlgebra.Matrix.Reindex Mathlib.RingTheory.LaurentSeries Mathlib.NumberTheory.ModularForms.Identities Mathlib.MeasureTheory.Function.ContinuousMapDense Mathlib.Analysis.Complex.Periodic Mathlib.Geometry.Manifold.ContMDiffMap Mathlib.NumberTheory.NumberField.Norm 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.Analysis.Fourier.FiniteAbelian.PontryaginDuality Mathlib.Analysis.FunctionalSpaces.SobolevInequality Mathlib.LinearAlgebra.QuadraticForm.Prod Mathlib.RingTheory.Trace.Basic Mathlib.NumberTheory.LSeries.ZMod Mathlib.Analysis.CStarAlgebra.Module.Constructions Mathlib.Probability.Distributions.Exponential Mathlib.RingTheory.WittVector.MulCoeff Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric Mathlib.Analysis.SpecialFunctions.Complex.Arctan Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation Mathlib.Analysis.BoxIntegral.Partition.Measure Mathlib.LinearAlgebra.Charpoly.ToMatrix Mathlib.FieldTheory.Normal Mathlib.GroupTheory.Perm.Closure Mathlib.Analysis.Fourier.AddCircleMulti Mathlib.Probability.Martingale.Upcrossing Mathlib.MeasureTheory.Function.SimpleFuncDenseLp Mathlib.Analysis.RCLike.Lemmas Mathlib.Probability.Martingale.OptionalSampling Mathlib.RingTheory.Norm.Defs Mathlib.RingTheory.Kaehler.Polynomial Mathlib.Analysis.RCLike.Inner Mathlib.RingTheory.WittVector.Identities Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap Mathlib.Analysis.Convex.GaugeRescale Mathlib.LinearAlgebra.RootSystem.RootPairingCat Mathlib.FieldTheory.Adjoin Mathlib.MeasureTheory.Integral.DivergenceTheorem Mathlib.LinearAlgebra.ExteriorPower.Basic Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact Mathlib.Analysis.SpecialFunctions.Log.NegMulLog Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion Mathlib.Analysis.Calculus.BumpFunction.Basic Mathlib.NumberTheory.NumberField.EquivReindex 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.RingTheory.WittVector.Truncated Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots Mathlib.NumberTheory.SiegelsLemma Mathlib.LinearAlgebra.JordanChevalley Mathlib.Analysis.SpecialFunctions.ImproperIntegrals Mathlib.AlgebraicGeometry.Noetherian Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties Mathlib.Analysis.InnerProductSpace.Dual Mathlib.FieldTheory.ChevalleyWarning Mathlib.RingTheory.Polynomial.Hermite.Gaussian Mathlib.FieldTheory.IsAlgClosed.Classification Mathlib.LinearAlgebra.QuadraticForm.Basic Mathlib.Analysis.Calculus.AddTorsor.Coord Mathlib.LinearAlgebra.QuadraticForm.Basis Mathlib.AlgebraicGeometry.EllipticCurve.Affine Mathlib.AlgebraicGeometry.EllipticCurve.Group Mathlib.RingTheory.RingHom.StandardSmooth Mathlib.LinearAlgebra.Matrix.Determinant.Misc Mathlib.Algebra.Module.Presentation.Differentials Mathlib.Analysis.Fourier.ZMod Mathlib.Analysis.SpecialFunctions.Complex.LogBounds Mathlib.NumberTheory.ModularForms.SlashActions Mathlib.Analysis.SpecialFunctions.Gamma.Deligne Mathlib.Analysis.Complex.PhragmenLindelof Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat Mathlib.Analysis.Calculus.SmoothSeries Mathlib.GroupTheory.Nilpotent Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff Mathlib.Analysis.InnerProductSpace.NormPow Mathlib.Algebra.Module.ZLattice.Basic Mathlib.Analysis.Convex.Intrinsic 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.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.MeasureTheory.Measure.Portmanteau 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.Analysis.Fourier.AddCircle Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation Mathlib.RingTheory.Nullstellensatz Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar Mathlib.Analysis.Calculus.MeanValue Mathlib.GroupTheory.SchurZassenhaus Mathlib.LinearAlgebra.Matrix.Polynomial Mathlib.Analysis.Calculus.LineDeriv.QuadraticMap Mathlib.Analysis.Fourier.Inversion Mathlib.Analysis.Normed.Algebra.QuaternionExponential Mathlib.Computability.AkraBazzi.AkraBazzi Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly Mathlib.LinearAlgebra.Trace 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.MeasureTheory.Function.ConditionalExpectation.AEMeasurable Mathlib.FieldTheory.Fixed Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic Mathlib.RingTheory.Adjoin.Field Mathlib.GroupTheory.Perm.Fin Mathlib.Geometry.Euclidean.Sphere.Ptolemy Mathlib.AlgebraicGeometry.Pullbacks Mathlib.FieldTheory.Finite.Basic Mathlib.Topology.Algebra.Module.FiniteDimension Mathlib.Analysis.Normed.Algebra.MatrixExponential Mathlib.RingTheory.IntegralClosure.IntegralRestrict Mathlib.Analysis.Calculus.Taylor Mathlib.MeasureTheory.Group.AddCircle Mathlib.Probability.Independence.ZeroOne Mathlib.Analysis.SpecialFunctions.Complex.Analytic 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.GroupTheory.Perm.Cycle.Factors 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.Probability.Distributions.Gaussian Mathlib.NumberTheory.LSeries.Injectivity Mathlib.Probability.Kernel.CondDistrib Mathlib.Analysis.Calculus.FDeriv.Measurable Mathlib.Analysis.Calculus.UniformLimitsDeriv Mathlib.RingTheory.RootsOfUnity.Lemmas Mathlib.NumberTheory.ModularForms.LevelOne Mathlib.MeasureTheory.Integral.Bochner 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.Probability.Martingale.Basic Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho Mathlib.FieldTheory.Finite.Polynomial Mathlib.NumberTheory.Cyclotomic.Gal Mathlib.Geometry.Manifold.IntegralCurve.Basic Mathlib.MeasureTheory.Decomposition.RadonNikodym Mathlib.Probability.Kernel.RadonNikodym Mathlib.RingTheory.Kaehler.CotangentComplex Mathlib.NumberTheory.Harmonic.GammaDeriv Mathlib.Geometry.Manifold.InteriorBoundary Mathlib.Analysis.InnerProductSpace.Subspace Mathlib.FieldTheory.Extension Mathlib.LinearAlgebra.Orientation Mathlib.NumberTheory.LSeries.Basic Mathlib.Geometry.Manifold.ContMDiffMFDeriv Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone 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.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.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.RepresentationTheory.Invariants Mathlib.RingTheory.Valuation.Integral Mathlib.FieldTheory.RatFunc.AsPolynomial Mathlib.MeasureTheory.Order.UpperLower Mathlib.Analysis.Calculus.ParametricIntegral Mathlib.MeasureTheory.Function.AEEqFun.DomAct Mathlib.Probability.Martingale.Convergence Mathlib.FieldTheory.KrullTopology Mathlib.Analysis.Complex.UpperHalfPlane.Metric Mathlib.RingTheory.LittleWedderburn Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner Mathlib.RingTheory.Unramified.Pi Mathlib.Algebra.Lie.LieTheorem Mathlib.AlgebraicGeometry.Morphisms.Separated Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable Mathlib.CategoryTheory.Preadditive.Schur Mathlib.Analysis.InnerProductSpace.Basic Mathlib.RingTheory.Generators Mathlib.Probability.Kernel.Disintegration.CondCDF Mathlib.MeasureTheory.Function.AEEqOfIntegral Mathlib.Combinatorics.Extremal.RuzsaSzemeredi Mathlib.Data.Complex.Determinant Mathlib.Analysis.Complex.OperatorNorm Mathlib.Analysis.PSeriesComplex Mathlib.FieldTheory.Relrank Mathlib.Probability.Kernel.Disintegration.Density Mathlib.RingTheory.Polynomial.Cyclotomic.Basic Mathlib.RingTheory.Ideal.Norm.AbsNorm Mathlib.Analysis.InnerProductSpace.Completion Mathlib.Analysis.Convex.Integral Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace Mathlib.AlgebraicGeometry.RationalMap Mathlib.AlgebraicGeometry.Modules.Tilde Mathlib.AlgebraicGeometry.Morphisms.Finite Mathlib.FieldTheory.Galois.Profinite Mathlib.FieldTheory.LinearDisjoint Mathlib.AlgebraicGeometry.Cover.Over Mathlib.AlgebraicGeometry.PrimeSpectrum.Noetherian Mathlib.RingTheory.Ideal.Norm.RelNorm Mathlib.LinearAlgebra.CliffordAlgebra.Star Mathlib.LinearAlgebra.Projectivization.Constructions Mathlib.RingTheory.DiscreteValuationRing.TFAE Mathlib.NumberTheory.MulChar.Duality Mathlib.MeasureTheory.Integral.Prod Mathlib.NumberTheory.Cyclotomic.Embeddings Mathlib.MeasureTheory.Integral.Layercake Mathlib.Geometry.Euclidean.Circumcenter Mathlib.LinearAlgebra.Matrix.Nondegenerate Mathlib.Analysis.CStarAlgebra.Module.Defs Mathlib.LinearAlgebra.CrossProduct Mathlib.Analysis.Complex.Schwarz Mathlib.NumberTheory.LegendreSymbol.Basic Mathlib.Analysis.Fourier.FourierTransformDeriv Mathlib.RingTheory.Polynomial.Cyclotomic.Roots Mathlib.Analysis.Complex.UpperHalfPlane.Manifold Mathlib.LinearAlgebra.Matrix.Permutation Mathlib.LinearAlgebra.TensorProduct.Matrix Mathlib.FieldTheory.Finite.GaloisField Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic Mathlib.RepresentationTheory.Character Mathlib.AlgebraicGeometry.PrimeSpectrum.Module Mathlib.RingTheory.RingHom.FinitePresentation Mathlib.NumberTheory.LSeries.RiemannZeta Mathlib.MeasureTheory.Covering.OneDim Mathlib.Data.Real.Pi.Leibniz Mathlib.LinearAlgebra.QuadraticForm.Real Mathlib.LinearAlgebra.CliffordAlgebra.Equivs Mathlib.RingTheory.DedekindDomain.IntegralClosure Mathlib.Algebra.Order.Chebyshev Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing Mathlib.NumberTheory.FLT.Three Mathlib.FieldTheory.Galois.Basic Mathlib.RingTheory.WittVector.Verschiebung Mathlib.Geometry.Manifold.Algebra.SmoothFunctions Mathlib.Algebra.Lie.SkewAdjoint Mathlib.Geometry.Euclidean.Inversion.Calculus Mathlib.Analysis.Calculus.FirstDerivativeTest Mathlib.Analysis.InnerProductSpace.Positive Mathlib.LinearAlgebra.CliffordAlgebra.Fold Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody Mathlib.LinearAlgebra.Matrix.Charpoly.Basic Mathlib.Algebra.Lie.Weights.Chain Mathlib.NumberTheory.NumberField.Units.Basic Mathlib.RingTheory.Algebraic.Integral Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral Mathlib.Probability.Distributions.Uniform Mathlib.Geometry.Euclidean.Sphere.SecondInter Mathlib.Geometry.Euclidean.Basic Mathlib.Algebra.Lie.Matrix Mathlib.MeasureTheory.Covering.DensityTheorem 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.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.GroupTheory.FixedPointFree Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic Mathlib.AlgebraicGeometry.SpreadingOut Mathlib.AlgebraicGeometry.StructureSheaf 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.RingTheory.Smooth.Basic Mathlib.LinearAlgebra.CliffordAlgebra.Even Mathlib.AlgebraicGeometry.AffineSpace Mathlib.Combinatorics.Additive.Randomisation Mathlib.NumberTheory.LSeries.Dirichlet Mathlib.Analysis.InnerProductSpace.Projection Mathlib.NumberTheory.Fermat Mathlib.NumberTheory.Transcendental.Liouville.Residual Mathlib.MeasureTheory.Integral.Asymptotics Mathlib.LinearAlgebra.Matrix.AbsoluteValue Mathlib.LinearAlgebra.Eigenspace.Triangularizable 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.NumberTheory.ModularForms.JacobiTheta.TwoVariable Mathlib.LinearAlgebra.Matrix.BaseChange Mathlib.Analysis.Fourier.RiemannLebesgueLemma Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper Mathlib.Analysis.SpecialFunctions.SmoothTransition Mathlib.Analysis.BoxIntegral.Basic Mathlib.RingTheory.Valuation.LocalSubring Mathlib.GroupTheory.Perm.Cycle.Concrete Mathlib.Analysis.InnerProductSpace.Orthonormal Mathlib.Analysis.Quaternion Mathlib.Data.Matrix.Kronecker Mathlib.AlgebraicGeometry.FunctionField Mathlib.RingTheory.DedekindDomain.Different Mathlib.AlgebraicGeometry.Morphisms.Constructors Mathlib.Analysis.BoxIntegral.Integrability Mathlib.RingTheory.Discriminant Mathlib.NumberTheory.SumTwoSquares Mathlib.Analysis.InnerProductSpace.Calculus Mathlib.Topology.Category.TopCat.Sphere Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup Mathlib.Algebra.Module.PID 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.MeasureTheory.Integral.IntegralEqImproper Mathlib.Analysis.Complex.Polynomial.Basic Mathlib.RingTheory.DedekindDomain.SelmerGroup Mathlib.RingTheory.WittVector.StructurePolynomial Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic 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.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.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.NumberTheory.LegendreSymbol.JacobiSymbol Mathlib.RingTheory.Extension Mathlib.MeasureTheory.Function.Jacobian Mathlib.FieldTheory.Perfect Mathlib.AlgebraicGeometry.OpenImmersion Mathlib.NumberTheory.Transcendental.Lindemann.Init.AnalyticalPart Mathlib.Analysis.Complex.LocallyUniformLimit Mathlib.FieldTheory.IsAlgClosed.Basic Mathlib.NumberTheory.LSeries.Positivity Mathlib.FieldTheory.Minpoly.IsConjRoot Mathlib.Analysis.InnerProductSpace.EuclideanDist Mathlib.RingTheory.DedekindDomain.AdicValuation Mathlib.RingTheory.DedekindDomain.SInteger Mathlib.Analysis.Convex.Measure Mathlib.Probability.Moments Mathlib.NumberTheory.Harmonic.EulerMascheroni Mathlib.Analysis.SpecialFunctions.Log.Deriv Mathlib.NumberTheory.LegendreSymbol.AddCharacter Mathlib.FieldTheory.Cardinality 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.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.Topology.Instances.Matrix Mathlib.AlgebraicGeometry.AffineScheme Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup Mathlib.LinearAlgebra.CliffordAlgebra.Grading Mathlib.Data.Real.Pi.Bounds Mathlib.MeasureTheory.Decomposition.Lebesgue Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic Mathlib.Geometry.Manifold.MFDeriv.NormedSpace Mathlib.RingTheory.Polynomial.SeparableDegree Mathlib.FieldTheory.Separable Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation Mathlib.NumberTheory.KummerDedekind Mathlib.AlgebraicGeometry.Limits Mathlib.Geometry.Manifold.MFDeriv.Defs Mathlib.MeasureTheory.Function.LocallyIntegrable Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence Mathlib.RingTheory.Smooth.StandardSmooth Mathlib.LinearAlgebra.CliffordAlgebra.Basic Mathlib.FieldTheory.IsAlgClosed.Spectrum 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.FieldTheory.AlgebraicClosure Mathlib.Probability.Process.Stopping Mathlib.LinearAlgebra.CliffordAlgebra.CategoryTheory 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.NumberTheory.ClassNumber.FunctionField Mathlib.GroupTheory.Transfer Mathlib.RingTheory.Polynomial.Cyclotomic.Expand Mathlib.MeasureTheory.Integral.BoundedContinuousFunction Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty 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.RingTheory.WittVector.Isocrystal Mathlib.Geometry.Manifold.IntegralCurve.UniformTime 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.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.MeasureTheory.VectorMeasure.WithDensity Mathlib.LinearAlgebra.Reflection Mathlib.LinearAlgebra.AnnihilatingPolynomial Mathlib.MeasureTheory.Constructions.HaarToSphere Mathlib.Analysis.SpecialFunctions.JapaneseBracket Mathlib.RingTheory.Valuation.AlgebraInstances 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.ZetaValues Mathlib.Analysis.Convex.Deriv Mathlib.NumberTheory.Cyclotomic.Basic Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine Mathlib.Analysis.SpecialFunctions.Arsinh Mathlib.Analysis.Complex.Positivity Mathlib.Analysis.Calculus.ContDiff.FiniteDimension Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure Mathlib.Analysis.Fourier.FourierTransform 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.RingTheory.Smooth.Pi Mathlib.RingTheory.LocalProperties.IntegrallyClosed Mathlib.Probability.IdentDistrib Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances Mathlib.RingTheory.Complex Mathlib.Analysis.Convolution Mathlib.AlgebraicGeometry.Scheme Mathlib.LinearAlgebra.Matrix.Adjugate Mathlib.LinearAlgebra.Matrix.SchurComplement Mathlib.RingTheory.Etale.Pi Mathlib.LinearAlgebra.Eigenspace.Semisimple Mathlib.Analysis.Calculus.Conformal.InnerProduct Mathlib.Analysis.Calculus.VectorField Mathlib.FieldTheory.KummerExtension Mathlib.RingTheory.Polynomial.Cyclotomic.Eval Mathlib.AlgebraicGeometry.Gluing Mathlib.LinearAlgebra.QuadraticForm.Isometry Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty Mathlib.Analysis.Complex.Arg Mathlib.Geometry.Manifold.Algebra.Monoid Mathlib.FieldTheory.Minpoly.Field Mathlib.LinearAlgebra.UnitaryGroup Mathlib.Topology.Algebra.Module.Determinant Mathlib.Algebra.Module.LinearMap.Polynomial Mathlib.Analysis.MellinInversion Mathlib.RepresentationTheory.GroupCohomology.LowDegree Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear Mathlib.AlgebraicGeometry.Cover.Open Mathlib.Analysis.Convex.Cone.InnerDual Mathlib.Geometry.Manifold.Algebra.Structures Mathlib.AlgebraicGeometry.Stalk Mathlib.RingTheory.AdicCompletion.Algebra Mathlib.Analysis.CStarAlgebra.Hom Mathlib.Analysis.Complex.Polynomial.UnitTrinomial Mathlib.Geometry.Manifold.PartitionOfUnity Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian Mathlib.Analysis.Complex.UpperHalfPlane.Basic Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv Mathlib.Geometry.Manifold.MFDeriv.Atlas Mathlib.MeasureTheory.Measure.SeparableMeasure Mathlib.LinearAlgebra.Matrix.Basis Mathlib.MeasureTheory.Covering.Differentiation Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange Mathlib.GroupTheory.FiniteAbelian.Duality Mathlib.NumberTheory.LSeries.HurwitzZetaOdd Mathlib.GroupTheory.SpecificGroups.Alternating Mathlib.LinearAlgebra.QuadraticForm.TensorProduct Mathlib.ModelTheory.Algebra.Field.IsAlgClosed Mathlib.Analysis.Complex.Hadamard Mathlib.RingTheory.Etale.Basic 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.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.Probability.Distributions.Pareto Mathlib.NumberTheory.DirichletCharacter.Bounds Mathlib.Analysis.Convex.Cone.Closure Mathlib.MeasureTheory.Measure.Lebesgue.Integral Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality Mathlib.FieldTheory.PurelyInseparable Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv Mathlib.Analysis.Calculus.Gradient.Basic Mathlib.Algebra.Polynomial.Module.FiniteDimensional Mathlib.Analysis.Calculus.Rademacher Mathlib.Analysis.Calculus.BumpFunction.InnerProduct Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace Mathlib.LinearAlgebra.Matrix.Spectrum Mathlib.RingTheory.WittVector.IsPoly Mathlib.RingTheory.Kaehler.TensorProduct Mathlib.MeasureTheory.Integral.Pi Mathlib.NumberTheory.NumberField.House Mathlib.Analysis.Normed.Module.Complemented Mathlib.Analysis.InnerProductSpace.l2Space Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap Mathlib.Analysis.Complex.UpperHalfPlane.Exp Mathlib.NumberTheory.NumberField.Embeddings Mathlib.MeasureTheory.Function.Intersectivity 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.LinearAlgebra.SymplecticGroup Mathlib.Geometry.Manifold.AnalyticManifold Mathlib.Analysis.MellinTransform Mathlib.LinearAlgebra.Determinant Mathlib.LinearAlgebra.Matrix.Transvection 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.Analysis.Convex.SpecificFunctions.Deriv Mathlib.Analysis.Normed.Module.WeakDual Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd Mathlib.MeasureTheory.Integral.SetToL1 Mathlib.Analysis.Calculus.FDeriv.Symmetric Mathlib.RingTheory.WittVector.Defs Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear Mathlib.Geometry.Euclidean.Inversion.Basic Mathlib.Algebra.Lie.Rank Mathlib.Probability.Kernel.Condexp 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.GroupTheory.Perm.ConjAct Mathlib.LinearAlgebra.CliffordAlgebra.Prod Mathlib.AlgebraicGeometry.GluingOneHypercover Mathlib.LinearAlgebra.Eigenspace.Pi Mathlib.FieldTheory.Galois.Infinite Mathlib.Algebra.Lie.Classical Mathlib.NumberTheory.LSeries.PrimesInAP 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.Geometry.Manifold.Algebra.LeftInvariantDerivation Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension Mathlib.Analysis.Complex.IntegerCompl Mathlib.Probability.Distributions.Gamma Mathlib.LinearAlgebra.Eigenspace.Zero Mathlib.Probability.Martingale.OptionalStopping Mathlib.Probability.Martingale.BorelCantelli Mathlib.Analysis.SpecialFunctions.ExpDeriv Mathlib.Geometry.Manifold.DerivationBundle Mathlib.LinearAlgebra.Eigenspace.Minpoly Mathlib.Probability.Density 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.Geometry.Manifold.IntegralCurve.Transform Mathlib.Analysis.ODE.PicardLindelof 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.GroupTheory.Frattini Mathlib.RingTheory.WittVector.DiscreteValuationRing Mathlib.Geometry.Manifold.LocalDiffeomorph Mathlib.FieldTheory.PolynomialGaloisGroup Mathlib.Algebra.CharP.CharAndCard Mathlib.Analysis.InnerProductSpace.Orientation Mathlib.Geometry.Euclidean.Angle.Oriented.Affine Mathlib.GroupTheory.PGroup Mathlib.NumberTheory.ModularForms.CongruenceSubgroups Mathlib.RingTheory.DedekindDomain.PID 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.MeasureTheory.Group.Integral Mathlib.LinearAlgebra.Matrix.IsDiag Mathlib.RingTheory.Norm.Transitivity Mathlib.FieldTheory.SplittingField.Construction Mathlib.MeasureTheory.Measure.Haar.Disintegration Mathlib.LinearAlgebra.Charpoly.BaseChange Mathlib.Algebra.Lie.Weights.Linear Mathlib.RingTheory.Unramified.Finite Mathlib.LinearAlgebra.Matrix.Determinant.Basic Mathlib.RingTheory.Kaehler.JacobiZariski Mathlib.Probability.Integration Mathlib.Analysis.Distribution.SchwartzSpace Mathlib.GroupTheory.Perm.Cycle.Type 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.Matrix.NonsingularInverse Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski Mathlib.Analysis.SpecialFunctions.Pow.Integral Mathlib.Geometry.Manifold.WhitneyEmbedding Mathlib.FieldTheory.RatFunc.Degree Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis Mathlib.Algebra.Lie.CartanExists Mathlib.RingTheory.Localization.Away.AdjoinRoot 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.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic Mathlib.MeasureTheory.Function.ConditionalExpectation.Real Mathlib.LinearAlgebra.Matrix.FixedDetMatrices Mathlib.RingTheory.Perfection Mathlib.RingTheory.Norm.Basic Mathlib.Data.Real.Pi.Wallis 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.NumberTheory.EulerProduct.ExpLog Mathlib.RingTheory.AlgebraicIndependent.Adjoin Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique Mathlib.GroupTheory.SpecificGroups.ZGroup Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular 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.Analysis.Calculus.ContDiff.WithLp Mathlib.LinearAlgebra.QuadraticForm.Dual Mathlib.AlgebraicGeometry.Morphisms.Etale Mathlib.NumberTheory.ModularForms.QExpansion Mathlib.MeasureTheory.Measure.Haar.Quotient Mathlib.Geometry.Manifold.Instances.Sphere Mathlib.LinearAlgebra.Matrix.Block Mathlib.Geometry.Manifold.VectorBundle.SmoothSection Mathlib.Geometry.Manifold.ContMDiff.Product Mathlib.LinearAlgebra.RootSystem.Defs Mathlib.Analysis.InnerProductSpace.LaxMilgram Mathlib.RingTheory.WittVector.MulP Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate Mathlib.Data.Nat.Factorial.SuperFactorial
 1

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

@Komyyy Komyyy mentioned this pull request Jan 6, 2025
Closed
1 task
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jan 6, 2025
YaelDillies
YaelDillies approved these changes Jan 6, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

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

Thanks! That's a very clear improvement

maintainer delegate

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jan 6, 2025

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jan 6, 2025
@fpvandoorn
Copy link
Copy Markdown
Member

fpvandoorn commented Jan 6, 2025

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jan 6, 2025

✌️ Komyyy can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@ghost ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jan 6, 2025
@Komyyy @YaelDillies
suggestion
e349bf7 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@Komyyy
Copy link
Copy Markdown
Contributor Author

Komyyy commented Jan 7, 2025

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Jan 7, 2025
@Komyyy
perf: improves the performance of the Repr (Equiv.Perm α) instance …
ff91822 
…(1/4) (#20519)

This PR reduces computation time from $O(n^2)$ (more precisery, $O(\sum_{k<n} k)$.) to $O(n)$ by using `List.iterate`.



Co-authored-by: Miyahara Kō <52843868+Komyyy@users.noreply.github.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jan 7, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title perf: improves the performance of the Repr (Equiv.Perm α) instance (1/4) [Merged by Bors] - perf: improves the performance of the Repr (Equiv.Perm α) instance (1/4) Jan 7, 2025
@mathlib-bors mathlib-bors bot closed this Jan 7, 2025
@mathlib-bors mathlib-bors bot deleted the Komyyy/Equiv.Perm.instRepr3 branch January 7, 2025 02:45
@Komyyy Komyyy mentioned this pull request Jan 7, 2025
Closed
1 task
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

@YaelDillies YaelDillies YaelDillies approved these changes

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@Komyyy @fpvandoorn @YaelDillies