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

chore(Subalgebra/Unitization): move unrelated defs/lemmas earlier #20526

Open
wants to merge 3 commits into
base: master
Choose a base branch
from
Open

chore(Subalgebra/Unitization): move unrelated defs/lemmas earlier #20526

wants to merge 3 commits into from
+152 −183

Conversation

YaelDillies
Copy link
Collaborator

@YaelDillies YaelDillies commented Jan 6, 2025 •
edited
Loading

The Subobject.toNonUnitalSubobject and NonUnitalSubobject.toSubobject functions (for Subobject = Subsemiring, Subring, Subalgebra, StarSubalgebra) were in Algebra.Algebra.Subalgebra.Unitization instead of where Subobject is defined. This PR moves them there, at the cost of importing NonUnitalSubobject when defining Subobject (which seems like a fine trade-off).

Motivation: The current situation made #16094 have an immense import increase.

Open in Gitpod

@YaelDillies
chore(Subalgebra/Unitization): move unrelated defs/lemmas earlier
ae081e9 
The `Subobject.toNonUnitalSubobject` and `NonUnitalSubobject.toSubobject` functions (for `Subobject` = `Subsemiring`, `Subring`, `Subalgebra`, `StarSubalgebra`) were in `Algebra.Algebra.Subalgebra.Unitization` instead of where `Subobject` is defined. This PR moves them there, at the cost of importing `NonUnitalSubobject` when defining `Subobject` (which seems like a fine trade-off).
@github-actions GitHub Actions
Copy link

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

PR summary d0976fbd83

Import changes for modified files

Dependency changes

File Base Count Head Count Change
Mathlib.Algebra.Star.Subalgebra 936 940 +4 (+0.43%)
Mathlib.Algebra.Algebra.Subalgebra.Basic 910 913 +3 (+0.33%)
Mathlib.RingTheory.Adjoin.Basic 921 924 +3 (+0.33%)
Mathlib.Topology.ContinuousMap.StoneWeierstrass 1596 1594 -2 (-0.13%)
Import changes for all files
Files Import difference
24 files Mathlib.NumberTheory.LSeries.HurwitzZetaValues Mathlib.NumberTheory.Harmonic.ZetaAsymp Mathlib.Analysis.Fourier.PoissonSummation Mathlib.Analysis.Distribution.FourierSchwartz Mathlib.NumberTheory.EulerProduct.DirichletLSeries Mathlib.NumberTheory.LSeries.DirichletContinuation Mathlib.NumberTheory.LSeries.ZMod Mathlib.Analysis.Fourier.AddCircleMulti Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold Mathlib.NumberTheory.LSeries.HurwitzZetaEven Mathlib.Analysis.Fourier.AddCircle Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable Mathlib.Analysis.Fourier.FourierTransformDeriv Mathlib.NumberTheory.LSeries.RiemannZeta Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds Mathlib.NumberTheory.LSeries.Dirichlet Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable Mathlib.NumberTheory.LSeries.Nonvanishing Mathlib.NumberTheory.ZetaValues Mathlib.Topology.ContinuousMap.StoneWeierstrass Mathlib.NumberTheory.LSeries.HurwitzZetaOdd Mathlib.NumberTheory.LSeries.PrimesInAP Mathlib.NumberTheory.LSeries.HurwitzZeta
 -2
14 files Mathlib.Analysis.CStarAlgebra.GelfandDuality Mathlib.Analysis.CStarAlgebra.Module.Constructions Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart Mathlib.Analysis.CStarAlgebra.Module.Defs Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique Mathlib.Analysis.CStarAlgebra.ApproximateUnit Mathlib.Analysis.InnerProductSpace.StarOrder Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances Mathlib.Analysis.CStarAlgebra.Hom Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
 -1
557 files Mathlib.MeasureTheory.Integral.VitaliCaratheodory Mathlib.Analysis.MeanInequalitiesPow Mathlib.Combinatorics.SimpleGraph.Triangle.Removal Mathlib.Analysis.BoxIntegral.UnitPartition Mathlib.Probability.Process.HittingTime Mathlib.Analysis.InnerProductSpace.Spectrum Mathlib.Analysis.InnerProductSpace.Symmetric Mathlib.Analysis.InnerProductSpace.OfNorm Mathlib.NumberTheory.Cyclotomic.Rat Mathlib.Probability.BorelCantelli Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv Mathlib.Dynamics.TopologicalEntropy.NetEntropy Mathlib.Analysis.SpecialFunctions.Gamma.Basic Mathlib.NumberTheory.Padics.MahlerBasis Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual Mathlib.Probability.Variance Mathlib.Analysis.Complex.Angle Mathlib.LinearAlgebra.Matrix.PosDef Mathlib.Analysis.SpecialFunctions.Integrals Mathlib.Dynamics.Ergodic.AddCircle Mathlib.Analysis.Calculus.BumpFunction.Convolution Mathlib.Analysis.InnerProductSpace.Rayleigh Mathlib.Analysis.Normed.Module.Dual Mathlib.NumberTheory.NumberField.Discriminant.Basic Mathlib.NumberTheory.Cyclotomic.Discriminant Mathlib.NumberTheory.MulChar.Lemmas Mathlib.Analysis.Calculus.Deriv.Abs Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds Mathlib.Analysis.SpecialFunctions.Pow.Complex Mathlib.MeasureTheory.Measure.FiniteMeasure Mathlib.Tactic.FunProp.ContDiff Mathlib.MeasureTheory.Function.SpecialFunctions.Basic Mathlib.MeasureTheory.Integral.IntervalAverage Mathlib.Analysis.Normed.Lp.PiLp Mathlib.Analysis.Calculus.ParametricIntervalIntegral Mathlib.MeasureTheory.Measure.ProbabilityMeasure Mathlib.MeasureTheory.Function.UnifTight Mathlib.Analysis.SpecialFunctions.CompareExp Mathlib.NumberTheory.GaussSum Mathlib.Combinatorics.Derangements.Exponential Mathlib.Combinatorics.Additive.Corner.Roth Mathlib.MeasureTheory.Function.LpSeminorm.Basic Mathlib.MeasureTheory.Measure.Lebesgue.Complex Mathlib.Analysis.SpecialFunctions.Complex.Log Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology Mathlib.MeasureTheory.Integral.IntervalIntegral Mathlib.Topology.ContinuousMap.Polynomial Mathlib.Analysis.Calculus.FDeriv.WithLp Mathlib.Analysis.Complex.AbsMax Mathlib.Analysis.InnerProductSpace.ProdL2 Mathlib.Probability.Kernel.Disintegration.CDFToKernel Mathlib.Geometry.Manifold.Instances.Real Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv Mathlib.Geometry.Manifold.Complex Mathlib.MeasureTheory.Integral.CircleIntegral Mathlib.Probability.StrongLaw Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral Mathlib.Analysis.Complex.HalfPlane Mathlib.Probability.Kernel.Composition.MeasureCompProd Mathlib.Probability.Kernel.Composition.IntegralCompProd Mathlib.Analysis.SpecialFunctions.Gamma.Beta Mathlib.MeasureTheory.Integral.TorusIntegral Mathlib.Analysis.Complex.Isometry Mathlib.MeasureTheory.Function.L2Space Mathlib.MeasureTheory.Measure.LevyProkhorovMetric Mathlib.Analysis.Complex.UnitDisc.Basic Mathlib.Analysis.SpecialFunctions.Exp Mathlib.Algebra.Module.ZLattice.Covolume Mathlib.NumberTheory.ModularForms.Identities Mathlib.MeasureTheory.Function.ContinuousMapDense Mathlib.Analysis.Complex.Periodic Mathlib.Analysis.Normed.Algebra.Norm Mathlib.Computability.AkraBazzi.GrowsPolynomially Mathlib.Analysis.NormedSpace.RCLike Mathlib.Analysis.Complex.TaylorSeries Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality Mathlib.Analysis.FunctionalSpaces.SobolevInequality Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan Mathlib.Probability.Distributions.Exponential Mathlib.Analysis.SpecialFunctions.Complex.Arctan Mathlib.Analysis.BoxIntegral.Partition.Measure Mathlib.Probability.Martingale.Upcrossing Mathlib.MeasureTheory.Function.SimpleFuncDenseLp Mathlib.Analysis.RCLike.Lemmas Mathlib.Probability.Martingale.OptionalSampling Mathlib.Analysis.RCLike.Inner Mathlib.Analysis.Convex.GaugeRescale Mathlib.MeasureTheory.Integral.DivergenceTheorem Mathlib.Analysis.SpecialFunctions.Log.NegMulLog Mathlib.NumberTheory.NumberField.EquivReindex Mathlib.LinearAlgebra.Matrix.Gershgorin Mathlib.MeasureTheory.Measure.LogLikelihoodRatio Mathlib.Analysis.Complex.Circle Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots Mathlib.NumberTheory.SiegelsLemma Mathlib.Analysis.SpecialFunctions.PolynomialExp Mathlib.Analysis.SpecialFunctions.ImproperIntegrals Mathlib.Analysis.InnerProductSpace.Dual Mathlib.RingTheory.Polynomial.Hermite.Gaussian Mathlib.NumberTheory.SumPrimeReciprocals Mathlib.MeasureTheory.Function.LpSeminorm.Trim Mathlib.Analysis.PSeries 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.Analysis.Calculus.SmoothSeries Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff Mathlib.Analysis.InnerProductSpace.NormPow Mathlib.Algebra.Module.ZLattice.Basic Mathlib.Analysis.Complex.Basic Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls Mathlib.MeasureTheory.Integral.FundThmCalculus Mathlib.NumberTheory.Cyclotomic.Three Mathlib.Probability.Kernel.Disintegration.Integral Mathlib.Analysis.CStarAlgebra.Matrix Mathlib.Geometry.Manifold.PoincareConjecture Mathlib.MeasureTheory.Measure.Portmanteau Mathlib.NumberTheory.LSeries.Deriv Mathlib.MeasureTheory.Measure.Haar.NormedSpace Mathlib.Topology.ContinuousMap.Bounded.Star Mathlib.Topology.ContinuousMap.Compact Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar Mathlib.Analysis.SpecialFunctions.Pow.Continuity Mathlib.Analysis.Calculus.MeanValue Mathlib.Analysis.Fourier.Inversion Mathlib.Analysis.Normed.Algebra.QuaternionExponential Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality Mathlib.Computability.AkraBazzi.AkraBazzi Mathlib.NumberTheory.NumberField.Completion Mathlib.Probability.Kernel.WithDensity Mathlib.Analysis.SpecialFunctions.NonIntegrable Mathlib.Geometry.Euclidean.Angle.Oriented.Basic Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable Mathlib.Geometry.Euclidean.Sphere.Ptolemy Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp Mathlib.Analysis.Normed.Algebra.MatrixExponential 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.Analysis.LocallyConvex.WeakSpace Mathlib.Analysis.Calculus.LHopital Mathlib.Analysis.Convex.Cone.Pointed Mathlib.Probability.Kernel.Disintegration.StandardBorel Mathlib.MeasureTheory.Function.UniformIntegrable Mathlib.MeasureTheory.Measure.Hausdorff Mathlib.NumberTheory.ModularForms.SlashInvariantForms Mathlib.Probability.Distributions.Gaussian Mathlib.NumberTheory.LSeries.Injectivity Mathlib.Probability.Kernel.CondDistrib Mathlib.Analysis.SpecificLimits.FloorPow Mathlib.Analysis.Calculus.UniformLimitsDeriv Mathlib.NumberTheory.ModularForms.LevelOne Mathlib.MeasureTheory.Integral.Bochner Mathlib.Algebra.Order.AbsoluteValue.Equivalence Mathlib.MeasureTheory.Measure.Haar.Unique Mathlib.Geometry.Manifold.BumpFunction Mathlib.Analysis.Calculus.FDeriv.Extend Mathlib.Probability.Martingale.Basic Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho Mathlib.NumberTheory.Cyclotomic.Gal Mathlib.Analysis.Normed.Lp.ProdLp Mathlib.MeasureTheory.Decomposition.RadonNikodym Mathlib.Probability.Kernel.RadonNikodym Mathlib.NumberTheory.Harmonic.GammaDeriv Mathlib.Analysis.InnerProductSpace.Subspace Mathlib.NumberTheory.LSeries.Basic Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone Mathlib.Analysis.LocallyConvex.AbsConvex Mathlib.Analysis.Normed.Ring.SeminormFromConst Mathlib.MeasureTheory.Decomposition.SignedLebesgue Mathlib.NumberTheory.NumberField.ProductFormula Mathlib.MeasureTheory.Measure.WithDensityFinite Mathlib.Geometry.Euclidean.Sphere.Power Mathlib.Data.Real.Pi.Irrational Mathlib.Analysis.Complex.CauchyIntegral Mathlib.Analysis.InnerProductSpace.JointEigenspace Mathlib.Analysis.Normed.Group.Tannery Mathlib.Analysis.SpecialFunctions.Pow.Deriv Mathlib.MeasureTheory.Group.GeometryOfNumbers Mathlib.Analysis.SpecialFunctions.PolarCoord Mathlib.MeasureTheory.Covering.LiminfLimsup Mathlib.Geometry.Euclidean.Angle.Sphere Mathlib.Analysis.InnerProductSpace.LinearPMap Mathlib.Analysis.Complex.UpperHalfPlane.Topology Mathlib.Analysis.Complex.IsIntegral Mathlib.Analysis.SpecialFunctions.Log.Base Mathlib.MeasureTheory.Order.UpperLower Mathlib.Analysis.Calculus.ParametricIntegral Mathlib.Probability.Martingale.Convergence Mathlib.Analysis.Convex.SpecificFunctions.Pow Mathlib.Analysis.Complex.UpperHalfPlane.Metric Mathlib.RingTheory.LittleWedderburn Mathlib.Analysis.Normed.Lp.lpSpace Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner Mathlib.Analysis.Normed.Ring.Seminorm Mathlib.Analysis.InnerProductSpace.Basic Mathlib.Probability.Kernel.Disintegration.CondCDF Mathlib.MeasureTheory.Function.AEEqOfIntegral Mathlib.Combinatorics.Extremal.RuzsaSzemeredi Mathlib.Analysis.Complex.OperatorNorm Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov Mathlib.Analysis.PSeriesComplex Mathlib.Probability.Kernel.Disintegration.Density Mathlib.RingTheory.Polynomial.Cyclotomic.Basic Mathlib.Analysis.InnerProductSpace.Completion Mathlib.Analysis.Convex.Integral Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace Mathlib.MeasureTheory.Function.SpecialFunctions.Arctan Mathlib.Analysis.Normed.Group.ZeroAtInfty Mathlib.MeasureTheory.Integral.Prod Mathlib.NumberTheory.Cyclotomic.Embeddings Mathlib.MeasureTheory.Integral.Layercake Mathlib.Analysis.Complex.ReImTopology Mathlib.Geometry.Euclidean.Circumcenter Mathlib.Analysis.Complex.Schwarz Mathlib.RingTheory.Polynomial.Cyclotomic.Roots Mathlib.Analysis.Complex.UpperHalfPlane.Manifold Mathlib.Analysis.SpecialFunctions.Complex.Arg Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace Mathlib.MeasureTheory.Covering.OneDim Mathlib.Data.Real.Pi.Leibniz Mathlib.LinearAlgebra.QuadraticForm.Real Mathlib.NumberTheory.FLT.Three Mathlib.Geometry.Euclidean.Inversion.Calculus Mathlib.Analysis.Calculus.FirstDerivativeTest Mathlib.Analysis.InnerProductSpace.Positive Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody Mathlib.Topology.ContinuousMap.Units Mathlib.NumberTheory.NumberField.Units.Basic Mathlib.Probability.Distributions.Uniform Mathlib.Geometry.Euclidean.Sphere.SecondInter Mathlib.Geometry.Euclidean.Basic Mathlib.MeasureTheory.Covering.DensityTheorem Mathlib.Topology.ContinuousMap.StarOrdered Mathlib.Analysis.Analytic.RadiusLiminf Mathlib.MeasureTheory.Constructions.UnitInterval Mathlib.NumberTheory.DirichletCharacter.GaussSum Mathlib.LinearAlgebra.QuadraticForm.Complex Mathlib.MeasureTheory.Measure.FiniteMeasureProd Mathlib.Analysis.InnerProductSpace.Orthogonal Mathlib.Probability.Kernel.MeasurableIntegral Mathlib.Geometry.Euclidean.MongePoint Mathlib.Topology.CWComplex Mathlib.NumberTheory.Ostrowski Mathlib.MeasureTheory.Measure.Doubling Mathlib.Analysis.MeanInequalities Mathlib.Probability.Distributions.Poisson Mathlib.Geometry.Euclidean.Sphere.Basic Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable Mathlib.Analysis.Normed.Ring.SeminormFromBounded Mathlib.Combinatorics.Additive.Randomisation Mathlib.Analysis.InnerProductSpace.Projection Mathlib.NumberTheory.Fermat Mathlib.NumberTheory.Transcendental.Liouville.Residual Mathlib.MeasureTheory.Integral.Asymptotics Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike Mathlib.Tactic.NormNum.LegendreSymbol Mathlib.Geometry.Euclidean.Angle.Unoriented.Conformal Mathlib.Analysis.Convex.Strong Mathlib.Analysis.SpecialFunctions.BinaryEntropy Mathlib.Analysis.Complex.Asymptotics Mathlib.Analysis.Fourier.RiemannLebesgueLemma Mathlib.Analysis.SpecialFunctions.SmoothTransition Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse Mathlib.Analysis.BoxIntegral.Basic Mathlib.Analysis.InnerProductSpace.Orthonormal Mathlib.Analysis.Quaternion Mathlib.Analysis.SpecialFunctions.Bernstein Mathlib.Analysis.Normed.Algebra.Exponential Mathlib.MeasureTheory.Integral.RieszMarkovKakutani Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex Mathlib.Analysis.BoxIntegral.Integrability Mathlib.NumberTheory.SumTwoSquares Mathlib.Analysis.InnerProductSpace.Calculus Mathlib.Topology.Category.TopCat.Sphere Mathlib.Analysis.SpecialFunctions.Exponential Mathlib.Analysis.Convex.KreinMilman Mathlib.Analysis.Calculus.FDeriv.Norm Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp Mathlib.Combinatorics.Additive.AP.Three.Behrend Mathlib.NumberTheory.ClassNumber.Finite Mathlib.Topology.MetricSpace.GromovHausdorff Mathlib.Analysis.InnerProductSpace.Defs Mathlib.MeasureTheory.Integral.IntegralEqImproper Mathlib.Analysis.Complex.Polynomial.Basic Mathlib.MeasureTheory.Constructions.BorelSpace.Complex Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic Mathlib.Analysis.Complex.Tietze Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving Mathlib.MeasureTheory.Function.L1Space Mathlib.Analysis.NormedSpace.HahnBanach.Extension Mathlib.Probability.Kernel.Disintegration.Basic Mathlib.Analysis.Complex.RemovableSingularity Mathlib.MeasureTheory.Measure.Tilted Mathlib.Analysis.Complex.Liouville Mathlib.NumberTheory.Transcendental.Liouville.Measure Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum Mathlib.Analysis.InnerProductSpace.LinearMap Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle Mathlib.NumberTheory.LSeries.MellinEqDirichlet Mathlib.Analysis.InnerProductSpace.MeanErgodic Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol Mathlib.MeasureTheory.Function.Jacobian Mathlib.NumberTheory.Transcendental.Lindemann.Init.AnalyticalPart Mathlib.Analysis.Complex.LocallyUniformLimit Mathlib.NumberTheory.LSeries.Positivity Mathlib.Analysis.InnerProductSpace.EuclideanDist Mathlib.MeasureTheory.Function.LpOrder Mathlib.Analysis.Convex.Measure Mathlib.Probability.Moments Mathlib.NumberTheory.Harmonic.EulerMascheroni Mathlib.Analysis.SpecialFunctions.Log.Deriv Mathlib.NumberTheory.LegendreSymbol.AddCharacter Mathlib.NumberTheory.Cyclotomic.PID Mathlib.NumberTheory.JacobiSum.Basic Mathlib.Analysis.Normed.Lp.LpEquiv Mathlib.Topology.MetricSpace.HausdorffDimension Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff Mathlib.Analysis.RCLike.Basic Mathlib.Analysis.InnerProductSpace.PiL2 Mathlib.MeasureTheory.Group.FundamentalDomain Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane Mathlib.Analysis.Complex.Conformal Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity Mathlib.Topology.Instances.Complex Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup Mathlib.RingTheory.RootsOfUnity.Complex Mathlib.Topology.ContinuousMap.Weierstrass Mathlib.Analysis.SpecialFunctions.Log.Monotone Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics Mathlib.Data.Real.Pi.Bounds Mathlib.MeasureTheory.Decomposition.Lebesgue Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric Mathlib.Analysis.CStarAlgebra.Basic Mathlib.Topology.Algebra.PontryaginDual Mathlib.MeasureTheory.Function.LocallyIntegrable Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence Mathlib.Topology.MetricSpace.Holder Mathlib.NumberTheory.ModularForms.Basic Mathlib.Analysis.NormedSpace.HahnBanach.Separation Mathlib.Analysis.NormedSpace.DualNumber Mathlib.Probability.Process.Stopping Mathlib.MeasureTheory.Integral.PeakFunction Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 Mathlib.MeasureTheory.Function.SpecialFunctions.Inner Mathlib.NumberTheory.Modular Mathlib.NumberTheory.NumberField.Units.DirichletTheorem Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk Mathlib.NumberTheory.ClassNumber.FunctionField Mathlib.MeasureTheory.Integral.MeanInequalities Mathlib.RingTheory.Polynomial.Cyclotomic.Expand Mathlib.MeasureTheory.Integral.BoundedContinuousFunction Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty Mathlib.MeasureTheory.Integral.ExpDecay Mathlib.Dynamics.Ergodic.Action.OfMinimal 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.Analysis.Fourier.FiniteAbelian.Orthogonality Mathlib.Analysis.ConstantSpeed Mathlib.Analysis.LocallyConvex.WeakOperatorTopology Mathlib.LinearAlgebra.Matrix.Hermitian Mathlib.Analysis.Calculus.Monotone Mathlib.RingTheory.Polynomial.Selmer Mathlib.Topology.ContinuousMap.ContinuousMapZero Mathlib.Analysis.SumIntegralComparisons Mathlib.MeasureTheory.VectorMeasure.WithDensity Mathlib.MeasureTheory.Constructions.HaarToSphere Mathlib.Analysis.SpecialFunctions.JapaneseBracket Mathlib.MeasureTheory.Integral.CircleTransform Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent Mathlib.MeasureTheory.Integral.DominatedConvergence Mathlib.Analysis.NormedSpace.Extend Mathlib.NumberTheory.VonMangoldt Mathlib.Analysis.Convex.Deriv Mathlib.NumberTheory.Cyclotomic.Basic Mathlib.Analysis.CStarAlgebra.Exponential Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine Mathlib.Topology.MetricSpace.HolderNorm Mathlib.Analysis.SpecialFunctions.Arsinh Mathlib.Analysis.Complex.Positivity Mathlib.MeasureTheory.Function.ConvergenceInMeasure Mathlib.Analysis.Fourier.FourierTransform Mathlib.LinearAlgebra.Matrix.LDL Mathlib.Tactic.FunProp.Differentiable Mathlib.Probability.Independence.Integrable Mathlib.Analysis.Matrix Mathlib.Analysis.SpecialFunctions.Pow.Real Mathlib.Probability.IdentDistrib Mathlib.Dynamics.TopologicalEntropy.Semiconj Mathlib.Analysis.Convolution Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle Mathlib.LinearAlgebra.Matrix.SchurComplement Mathlib.Analysis.Convex.Gauge Mathlib.Analysis.Calculus.Conformal.InnerProduct Mathlib.Analysis.Calculus.VectorField Mathlib.RingTheory.Polynomial.Cyclotomic.Eval Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty Mathlib.Analysis.Complex.Arg Mathlib.Topology.MetricSpace.Kuratowski Mathlib.Analysis.MellinInversion Mathlib.Analysis.Convex.Cone.InnerDual Mathlib.Analysis.Complex.Polynomial.UnitTrinomial Mathlib.Geometry.Manifold.PartitionOfUnity Mathlib.Analysis.Complex.Convex Mathlib.Analysis.Complex.UpperHalfPlane.Basic Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs Mathlib.MeasureTheory.Measure.SeparableMeasure Mathlib.Analysis.Normed.Ring.IsPowMulFaithful Mathlib.MeasureTheory.Covering.Differentiation Mathlib.Analysis.LocallyConvex.ContinuousOfBounded Mathlib.Analysis.Complex.Hadamard Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts Mathlib.NumberTheory.PrimesCongruentOne Mathlib.Combinatorics.SimpleGraph.LapMatrix Mathlib.Analysis.BoundedVariation Mathlib.Analysis.InnerProductSpace.Adjoint Mathlib.Analysis.InnerProductSpace.Semisimple Mathlib.Combinatorics.SimpleGraph.Regularity.Bound Mathlib.NumberTheory.WellApproximable Mathlib.MeasureTheory.Measure.Lebesgue.Basic Mathlib.NumberTheory.LSeries.Convergence Mathlib.NumberTheory.Transcendental.Liouville.Basic Mathlib.Probability.Process.Adapted Mathlib.Analysis.Convex.Cone.Proper Mathlib.Probability.Distributions.Pareto Mathlib.Analysis.Convex.Cone.Closure Mathlib.MeasureTheory.Measure.Lebesgue.Integral Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv Mathlib.Analysis.Calculus.Gradient.Basic Mathlib.Analysis.Calculus.Rademacher Mathlib.Analysis.Calculus.BumpFunction.InnerProduct Mathlib.LinearAlgebra.Matrix.Spectrum Mathlib.MeasureTheory.Integral.Pi Mathlib.NumberTheory.NumberField.House Mathlib.Topology.ContinuousMap.CompactlySupported Mathlib.Analysis.InnerProductSpace.l2Space Mathlib.Analysis.Complex.UpperHalfPlane.Exp Mathlib.NumberTheory.NumberField.Embeddings Mathlib.MeasureTheory.Function.Intersectivity Mathlib.Dynamics.TopologicalEntropy.CoverEntropy Mathlib.Probability.Process.Filtration Mathlib.MeasureTheory.Integral.Periodic Mathlib.NumberTheory.Harmonic.Bounds Mathlib.Analysis.MellinTransform Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar Mathlib.NumberTheory.LSeries.Linearity Mathlib.MeasureTheory.Integral.Gamma 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.Geometry.Euclidean.Inversion.Basic Mathlib.Probability.Kernel.Condexp Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv Mathlib.Analysis.SpecialFunctions.Complex.Circle Mathlib.Topology.ContinuousMap.ZeroAtInfty Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma Mathlib.Geometry.Euclidean.Triangle Mathlib.MeasureTheory.Covering.Besicovitch Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension Mathlib.Analysis.Complex.IntegerCompl Mathlib.Probability.Distributions.Gamma Mathlib.Probability.Martingale.OptionalStopping Mathlib.Probability.Martingale.BorelCantelli Mathlib.Analysis.SpecialFunctions.ExpDeriv Mathlib.Probability.Density Mathlib.Dynamics.BirkhoffSum.NormedSpace Mathlib.Analysis.Complex.RealDeriv Mathlib.Analysis.Complex.OpenMapping Mathlib.Probability.ProbabilityMassFunction.Integrals Mathlib.Analysis.Calculus.BumpFunction.Normed Mathlib.Analysis.ODE.PicardLindelof Mathlib.NumberTheory.NumberField.ClassNumber Mathlib.Probability.ConditionalExpectation Mathlib.MeasureTheory.Integral.SetIntegral Mathlib.Analysis.SpecificLimits.RCLike Mathlib.Analysis.InnerProductSpace.ConformalLinearMap Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv Mathlib.Analysis.InnerProductSpace.Orientation Mathlib.Geometry.Euclidean.Angle.Oriented.Affine Mathlib.Analysis.SpecialFunctions.Pow.NNReal Mathlib.Tactic Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform Mathlib.MeasureTheory.Function.LpSpace.DomAct.Continuous Mathlib.Geometry.Euclidean.PerpBisector Mathlib.NumberTheory.NumberField.FinitePlaces Mathlib.Analysis.Convex.SpecificFunctions.Basic Mathlib.MeasureTheory.Group.Integral Mathlib.MeasureTheory.Measure.Haar.Disintegration Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic Mathlib.Probability.Integration Mathlib.Analysis.Distribution.SchwartzSpace Mathlib.NumberTheory.Bertrand Mathlib.MeasureTheory.Measure.Complex Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber Mathlib.Analysis.SpecialFunctions.Gamma.Deriv Mathlib.Analysis.BoxIntegral.DivergenceTheorem Mathlib.NumberTheory.LSeries.Convolution Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral Mathlib.Analysis.SpecialFunctions.Pow.Integral Mathlib.Geometry.Manifold.WhitneyEmbedding Mathlib.Topology.ContinuousMap.Ideals Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic Mathlib.Analysis.SpecialFunctions.Trigonometric.Series Mathlib.Probability.Kernel.Integral Mathlib.MeasureTheory.Integral.Average Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed Mathlib.Probability.Kernel.Disintegration.Unique Mathlib.Probability.Independence.Conditional Mathlib.Analysis.Complex.AbelLimit Mathlib.NumberTheory.AbelSummation Mathlib.MeasureTheory.Function.ConditionalExpectation.Real Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog Mathlib.RingTheory.Perfection Mathlib.Data.Real.Pi.Wallis Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt Mathlib.Probability.Process.PartitionFiltration Mathlib.Probability.Notation Mathlib.NumberTheory.LSeries.AbstractFuncEq Mathlib.Probability.CDF Mathlib.NumberTheory.EulerProduct.ExpLog Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps Mathlib.MeasureTheory.Measure.Haar.OfBasis Mathlib.Data.Complex.ExponentialBounds Mathlib.Analysis.InnerProductSpace.TwoDim Mathlib.NumberTheory.NumberField.AdeleRing Mathlib.Probability.Martingale.Centering Mathlib.Analysis.Calculus.ContDiff.WithLp Mathlib.NumberTheory.ModularForms.QExpansion Mathlib.MeasureTheory.Measure.Haar.Quotient Mathlib.Geometry.Manifold.Instances.Sphere Mathlib.Analysis.InnerProductSpace.LaxMilgram
 1
304 files Mathlib.RingTheory.FractionalIdeal.Norm Mathlib.Data.Real.Hyperreal Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion Mathlib.AlgebraicGeometry.Modules.Sheaf Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs Mathlib.FieldTheory.IsPerfectClosure Mathlib.FieldTheory.Finite.Trace Mathlib.MeasureTheory.Constructions.BorelSpace.Metric Mathlib.AlgebraicGeometry.Sites.Etale Mathlib.Probability.Kernel.Defs Mathlib.Topology.MetricSpace.Thickening Mathlib.AlgebraicGeometry.Morphisms.Proper Mathlib.AlgebraicGeometry.Morphisms.Preimmersion Mathlib.MeasureTheory.Integral.Marginal Mathlib.Topology.ContinuousMap.Star Mathlib.AlgebraicGeometry.PrimeSpectrum.TensorProduct Mathlib.FieldTheory.Laurent Mathlib.MeasureTheory.OuterMeasure.Caratheodory Mathlib.MeasureTheory.Constructions.BorelSpace.Basic Mathlib.Probability.ProbabilityMassFunction.Monad Mathlib.MeasureTheory.OuterMeasure.Induced Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic Mathlib.MeasureTheory.Measure.Regular Mathlib.MeasureTheory.Group.MeasurableEquiv Mathlib.AlgebraicGeometry.Sites.MorphismProperty Mathlib.AlgebraicGeometry.Sites.BigZariski Mathlib.RingTheory.Flat.Basic Mathlib.Data.Real.GoldenRatio Mathlib.MeasureTheory.Order.Lattice Mathlib.Analysis.Hofer Mathlib.RingTheory.Localization.NormTrace Mathlib.FieldTheory.AbelRuffini Mathlib.AlgebraicGeometry.Morphisms.Basic Mathlib.RingTheory.Regular.RegularSequence Mathlib.NumberTheory.NumberField.FractionalIdeal Mathlib.RingTheory.TensorProduct.Nontrivial Mathlib.AlgebraicGeometry.Morphisms.IsIso Mathlib.AlgebraicGeometry.Modules.Presheaf Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure Mathlib.MeasureTheory.Measure.AEDisjoint Mathlib.AlgebraicGeometry.PrimeSpectrum.FreeLocus Mathlib.RingTheory.LaurentSeries Mathlib.NumberTheory.NumberField.Norm Mathlib.ModelTheory.Algebra.Ring.Definability Mathlib.FieldTheory.Isaacs Mathlib.Topology.Compactification.OnePointEquiv Mathlib.RingTheory.Trace.Basic Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev Mathlib.MeasureTheory.Order.Group.Lattice Mathlib.Topology.Sheaves.CommRingCat Mathlib.FieldTheory.Normal Mathlib.MeasureTheory.Group.Measure Mathlib.Topology.ContinuousMap.Periodic Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits Mathlib.Topology.ContinuousMap.Lattice Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap Mathlib.FieldTheory.Adjoin Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion Mathlib.AlgebraicGeometry.Morphisms.Integral Mathlib.FieldTheory.SeparableClosure Mathlib.MeasureTheory.OuterMeasure.OfFunction Mathlib.AlgebraicGeometry.Noetherian Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties Mathlib.MeasureTheory.Covering.VitaliFamily Mathlib.FieldTheory.IsAlgClosed.Classification Mathlib.Algebra.Category.ModuleCat.Sheaf Mathlib.MeasureTheory.Measure.ContinuousPreimage Mathlib.RingTheory.RingHom.Flat Mathlib.MeasureTheory.Group.Arithmetic Mathlib.Probability.Kernel.Composition.ParallelComp Mathlib.Algebra.Category.ModuleCat.Sheaf.Free Mathlib.Dynamics.Ergodic.MeasurePreserving Mathlib.MeasureTheory.Function.AEMeasurableOrder Mathlib.RingTheory.Invariant Mathlib.AlgebraicGeometry.Sites.Small Mathlib.MeasureTheory.Category.MeasCat Mathlib.AlgebraicGeometry.Spec Mathlib.RingTheory.Unramified.Field Mathlib.RingTheory.Regular.IsSMulRegular Mathlib.FieldTheory.SeparableDegree Mathlib.FieldTheory.Minpoly.MinpolyDiv Mathlib.MeasureTheory.Constructions.Pi Mathlib.AlgebraicGeometry.ResidueField Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ Mathlib.RingTheory.Flat.Localization Mathlib.MeasureTheory.Decomposition.UnsignedHahn Mathlib.RingTheory.Nullstellensatz Mathlib.Dynamics.Ergodic.Conservative Mathlib.Analysis.BoxIntegral.Box.SubboxInduction Mathlib.AlgebraicGeometry.Over Mathlib.FieldTheory.Galois.GaloisClosure Mathlib.FieldTheory.Fixed Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic Mathlib.AlgebraicGeometry.Pullbacks Mathlib.RingTheory.IntegralClosure.IntegralRestrict Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable Mathlib.Topology.ContinuousMap.LocallyConstant Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme Mathlib.MeasureTheory.Measure.NullMeasurable Mathlib.FieldTheory.IsSepClosed Mathlib.AlgebraicGeometry.PrimeSpectrum.Jacobson Mathlib.MeasureTheory.Measure.Content Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings Mathlib.FieldTheory.Extension Mathlib.Combinatorics.Configuration Mathlib.AlgebraicGeometry.Properties Mathlib.MeasureTheory.Decomposition.Exhaustion Mathlib.MeasureTheory.Measure.Sub Mathlib.RingTheory.Etale.Field Mathlib.AlgebraicGeometry.Morphisms.Affine Mathlib.FieldTheory.AbsoluteGaloisGroup Mathlib.MeasureTheory.Measure.GiryMonad Mathlib.AlgebraicGeometry.Morphisms.Immersion Mathlib.Probability.ProbabilityMassFunction.Constructions Mathlib.RingTheory.Smooth.Local Mathlib.Probability.Kernel.Composition.Basic Mathlib.FieldTheory.RatFunc.AsPolynomial Mathlib.RingTheory.Flat.CategoryTheory Mathlib.NumberTheory.Rayleigh Mathlib.FieldTheory.KrullTopology Mathlib.Algebra.Category.ModuleCat.EnoughInjectives Mathlib.AlgebraicGeometry.Morphisms.Separated Mathlib.MeasureTheory.Measure.AbsolutelyContinuous Mathlib.Algebra.Category.Ring.LinearAlgebra Mathlib.Geometry.RingedSpace.OpenImmersion Mathlib.FieldTheory.Relrank Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits Mathlib.RingTheory.Ideal.Norm.AbsNorm Mathlib.AlgebraicGeometry.RationalMap Mathlib.AlgebraicGeometry.Modules.Tilde Mathlib.Probability.Kernel.Proper Mathlib.AlgebraicGeometry.Morphisms.Finite Mathlib.FieldTheory.Galois.Profinite Mathlib.MeasureTheory.Measure.Trim Mathlib.Analysis.Normed.Group.Completeness Mathlib.FieldTheory.LinearDisjoint Mathlib.AlgebraicGeometry.Cover.Over Mathlib.AlgebraicGeometry.PrimeSpectrum.Noetherian Mathlib.RingTheory.Ideal.Norm.RelNorm Mathlib.MeasureTheory.Decomposition.Jordan Mathlib.FieldTheory.Finite.GaloisField Mathlib.AlgebraicGeometry.PrimeSpectrum.Module Mathlib.RingTheory.DedekindDomain.IntegralClosure Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing Mathlib.FieldTheory.Galois.Basic Mathlib.LinearAlgebra.LinearDisjoint Mathlib.MeasureTheory.Group.LIntegral Mathlib.Probability.Kernel.Invariance Mathlib.Probability.ProbabilityMassFunction.Binomial Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology Mathlib.MeasureTheory.Group.Pointwise Mathlib.Data.Real.Irrational Mathlib.AlgebraicGeometry.SpreadingOut Mathlib.AlgebraicGeometry.StructureSheaf Mathlib.FieldTheory.PrimitiveElement Mathlib.AlgebraicGeometry.Morphisms.AffineAnd Mathlib.AlgebraicGeometry.AffineSpace Mathlib.RingTheory.Flat.FaithfullyFlat Mathlib.Probability.ConditionalProbability Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper Mathlib.Data.Complex.FiniteDimensional Mathlib.AlgebraicGeometry.FunctionField Mathlib.RingTheory.DedekindDomain.Different Mathlib.AlgebraicGeometry.Morphisms.Constructors Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian Mathlib.RingTheory.Discriminant Mathlib.MeasureTheory.Measure.Map Mathlib.RingTheory.DedekindDomain.SelmerGroup Mathlib.MeasureTheory.Measure.Count Mathlib.Probability.Kernel.Basic Mathlib.RingTheory.AdicCompletion.AsTensorProduct Mathlib.MeasureTheory.Group.AEStabilizer Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving Mathlib.AlgebraicGeometry.Morphisms.Smooth Mathlib.MeasureTheory.Measure.Comap Mathlib.Probability.ProbabilityMassFunction.Basic Mathlib.AlgebraicGeometry.OpenImmersion Mathlib.NumberTheory.DiophantineApproximation.ContinuedFractions Mathlib.Topology.MetricSpace.Contracting Mathlib.FieldTheory.IsAlgClosed.Basic Mathlib.FieldTheory.Minpoly.IsConjRoot Mathlib.Data.Complex.Cardinality Mathlib.RingTheory.DedekindDomain.AdicValuation Mathlib.RingTheory.DedekindDomain.SInteger Mathlib.Topology.Baire.BaireMeasurable Mathlib.Geometry.RingedSpace.LocallyRingedSpace Mathlib.FieldTheory.Cardinality Mathlib.AlgebraicGeometry.AffineScheme Mathlib.MeasureTheory.Group.Convolution Mathlib.Analysis.BoxIntegral.Partition.Filter Mathlib.Dynamics.Ergodic.Ergodic Mathlib.AlgebraicGeometry.Limits Mathlib.Algebra.Category.Ring.Under.Limits Mathlib.MeasureTheory.Measure.OpenPos Mathlib.MeasureTheory.Measure.Dirac Mathlib.Topology.Algebra.Valued.ValuationTopology Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated Mathlib.MeasureTheory.Decomposition.SignedHahn Mathlib.FieldTheory.AlgebraicClosure Mathlib.NumberTheory.NumberField.Basic Mathlib.FieldTheory.CardinalEmb Mathlib.Topology.MetricSpace.PiNat Mathlib.AlgebraicGeometry.PrimeSpectrum.Maximal Mathlib.RingTheory.WittVector.Isocrystal Mathlib.MeasureTheory.Measure.Stieltjes Mathlib.Dynamics.Ergodic.Action.Regular Mathlib.RingTheory.Trace.Quotient Mathlib.FieldTheory.NormalClosure Mathlib.Topology.MetricSpace.HausdorffDistance Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation Mathlib.Probability.Independence.Basic Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure Mathlib.Topology.MetricSpace.CantorScheme Mathlib.AlgebraicGeometry.Morphisms.FiniteType Mathlib.AlgebraicGeometry.Scheme Mathlib.RingTheory.Unramified.Locus Mathlib.MeasureTheory.Covering.Vitali Mathlib.RingTheory.Flat.EquationalCriterion Mathlib.MeasureTheory.VectorMeasure.Basic Mathlib.AlgebraicGeometry.Gluing Mathlib.Topology.Instances.Irrational Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber Mathlib.AlgebraicGeometry.Cover.Open Mathlib.AlgebraicGeometry.Stalk Mathlib.Data.Real.Cardinality Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification Mathlib.Analysis.Normed.Group.Pointwise Mathlib.ModelTheory.Algebra.Field.IsAlgClosed Mathlib.RingTheory.LinearDisjoint Mathlib.FieldTheory.JacobsonNoether Mathlib.MeasureTheory.Measure.Restrict Mathlib.RingTheory.LocalRing.Module Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality Mathlib.FieldTheory.PurelyInseparable Mathlib.MeasureTheory.Measure.MutuallySingular Mathlib.RingTheory.RingHom.Unramified Mathlib.Probability.Independence.Kernel Mathlib.MeasureTheory.Group.Prod Mathlib.MeasureTheory.Measure.Typeclasses Mathlib.AlgebraicGeometry.GammaSpecAdjunction Mathlib.RingTheory.Valuation.Minpoly Mathlib.RingTheory.Flat.Equalizer Mathlib.MeasureTheory.Measure.Prod Mathlib.Topology.Algebra.Valued.ValuedField Mathlib.Algebra.Algebra.Subalgebra.Directed Mathlib.Topology.ContinuousMap.Algebra Mathlib.AlgebraicGeometry.Cover.MorphismProperty Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks Mathlib.MeasureTheory.Measure.AEMeasurable Mathlib.MeasureTheory.Measure.WithDensity Mathlib.AlgebraicGeometry.GluingOneHypercover Mathlib.FieldTheory.Galois.Infinite Mathlib.MeasureTheory.Function.SimpleFuncDense Mathlib.Probability.Kernel.MeasurableLIntegral Mathlib.AlgebraicGeometry.ValuativeCriterion Mathlib.AlgebraicGeometry.Restrict Mathlib.AlgebraicGeometry.PullbackCarrier Mathlib.Dynamics.Ergodic.Action.Basic Mathlib.RingTheory.Flat.Stability Mathlib.MeasureTheory.Constructions.Projective Mathlib.MeasureTheory.Measure.MeasureSpace Mathlib.MeasureTheory.Measure.MeasureSpaceDef Mathlib.MeasureTheory.Group.Action Mathlib.AlgebraicGeometry.PrimeSpectrum.IsOpenComapC Mathlib.MeasureTheory.Function.AEMeasurableSequence Mathlib.RingTheory.WittVector.FrobeniusFractionField Mathlib.MeasureTheory.Measure.Haar.Basic Mathlib.FieldTheory.PolynomialGaloisGroup Mathlib.MeasureTheory.Constructions.BorelSpace.Real Mathlib.MeasureTheory.Constructions.BorelSpace.Order Mathlib.FieldTheory.AxGrothendieck Mathlib.MeasureTheory.Integral.Indicator Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed Mathlib.Topology.MetricSpace.Closeds Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous Mathlib.RingTheory.Unramified.Finite Mathlib.Analysis.SpecificLimits.Basic Mathlib.MeasureTheory.Function.EssSup Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent Mathlib.MeasureTheory.Function.Floor Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits Mathlib.FieldTheory.RatFunc.Degree Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis Mathlib.Probability.UniformOn Mathlib.MeasureTheory.Integral.Lebesgue Mathlib.RingTheory.Norm.Basic Mathlib.NumberTheory.FunctionField Mathlib.Topology.Baire.CompleteMetrizable Mathlib.MeasureTheory.Function.SimpleFunc Mathlib.MeasureTheory.Group.Defs Mathlib.RingTheory.AlgebraicIndependent.Adjoin Mathlib.AlgebraicGeometry.Morphisms.Etale Mathlib.Topology.Instances.RatLemmas Mathlib.NumberTheory.DiophantineApproximation.Basic Mathlib.Topology.Algebra.ContinuousMonoidHom
 2
616 files Mathlib.LinearAlgebra.FreeModule.Norm Mathlib.LinearAlgebra.Charpoly.Basic Mathlib.Algebra.Polynomial.FieldDivision Mathlib.Topology.Algebra.Module.Simple Mathlib.Combinatorics.Additive.ErdosGinzburgZiv Mathlib.RingTheory.Localization.Away.Lemmas Mathlib.RingTheory.IsAdjoinRoot Mathlib.NumberTheory.RamificationInertia.Basic Mathlib.RingTheory.DedekindDomain.Dvr Mathlib.RingTheory.Henselian Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Symmetric Mathlib.RingTheory.Algebraic.LinearIndependent Mathlib.NumberTheory.Wilson Mathlib.RingTheory.Polynomial.Content Mathlib.RepresentationTheory.GroupCohomology.Hilbert90 Mathlib.RingTheory.Localization.AtPrime Mathlib.RingTheory.PowerBasis Mathlib.Algebra.Symmetrized Mathlib.Algebra.Lie.Normalizer Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff Mathlib.LinearAlgebra.Matrix.ZPow Mathlib.RingTheory.SimpleModule Mathlib.Algebra.Category.FGModuleCat.Limits Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem Mathlib.LinearAlgebra.ExteriorAlgebra.Grading Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms Mathlib.RingTheory.Polynomial.Ideal Mathlib.RingTheory.PowerSeries.WellKnown Mathlib.Algebra.Module.Bimodule Mathlib.RingTheory.WittVector.Domain Mathlib.LinearAlgebra.Matrix.MvPolynomial Mathlib.Algebra.Category.Ring.Instances Mathlib.Algebra.Lie.Quotient Mathlib.RingTheory.AlgebraicIndependent.Transcendental Mathlib.LinearAlgebra.Dimension.DivisionRing Mathlib.LinearAlgebra.FreeModule.StrongRankCondition Mathlib.LinearAlgebra.BilinearForm.DualLattice Mathlib.RingTheory.DedekindDomain.Ideal Mathlib.RingTheory.Ideal.Over Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter Mathlib.RingTheory.GradedAlgebra.Noetherian Mathlib.RingTheory.LocalRing.Quotient Mathlib.Algebra.Category.ModuleCat.Differentials.Basic Mathlib.RingTheory.QuotSMulTop Mathlib.RingTheory.WittVector.InitTail Mathlib.RingTheory.Valuation.ExtendToLocalization Mathlib.LinearAlgebra.Dimension.Localization Mathlib.LinearAlgebra.Lagrange Mathlib.RingTheory.AdicCompletion.Basic Mathlib.Algebra.Ring.Subring.IntPolynomial Mathlib.RingTheory.TensorProduct.Finite Mathlib.LinearAlgebra.Coevaluation Mathlib.Algebra.Lie.Submodule Mathlib.RingTheory.ClassGroup Mathlib.LinearAlgebra.Matrix.Diagonal Mathlib.RingTheory.Derivation.Lie Mathlib.RingTheory.MvPowerSeries.LexOrder Mathlib.RingTheory.Algebraic.MvPolynomial Mathlib.Algebra.Module.DedekindDomain Mathlib.RingTheory.Trace.Defs Mathlib.Algebra.Polynomial.SpecificDegree Mathlib.Algebra.MvPolynomial.Counit Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots Mathlib.RingTheory.FractionalIdeal.Extended Mathlib.Algebra.MvPolynomial.Basic Mathlib.RingTheory.Adjoin.PowerBasis Mathlib.Algebra.Category.ModuleCat.ChangeOfRings Mathlib.Algebra.Polynomial.AlgebraMap Mathlib.RingTheory.Polynomial.Quotient Mathlib.RingTheory.AdicCompletion.Functoriality Mathlib.Algebra.CharP.LocalRing Mathlib.LinearAlgebra.PID Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits Mathlib.Algebra.MvPolynomial.Funext Mathlib.LinearAlgebra.FreeModule.Determinant Mathlib.RingTheory.Algebraic.Defs Mathlib.Algebra.Algebra.Subalgebra.Operations Mathlib.RingTheory.LocalRing.ResidueField.Ideal Mathlib.LinearAlgebra.QuadraticForm.Prod Mathlib.LinearAlgebra.TensorAlgebra.Grading Mathlib.RingTheory.Bialgebra.Hom Mathlib.RingTheory.WittVector.MulCoeff Mathlib.RingTheory.RingHom.FiniteType Mathlib.RingTheory.Artinian.Ring Mathlib.RingTheory.Algebraic.Cardinality Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation Mathlib.RingTheory.Localization.BaseChange Mathlib.LinearAlgebra.Charpoly.ToMatrix Mathlib.RingTheory.Ideal.Quotient.Noetherian Mathlib.RingTheory.DiscreteValuationRing.Basic Mathlib.NumberTheory.Zsqrtd.ToReal Mathlib.RingTheory.KrullDimension.Field Mathlib.RingTheory.Localization.Ideal Mathlib.LinearAlgebra.FreeModule.IdealQuotient Mathlib.RingTheory.Polynomial.Tower Mathlib.Algebra.Vertex.VertexOperator Mathlib.Algebra.Category.AlgebraCat.Limits Mathlib.Data.Nat.Choose.Lucas Mathlib.Algebra.Polynomial.Splits Mathlib.Algebra.Algebra.Subalgebra.Tower Mathlib.RingTheory.Localization.AsSubring Mathlib.RingTheory.Norm.Defs Mathlib.RingTheory.Kaehler.Polynomial Mathlib.RingTheory.Localization.Finiteness Mathlib.RingTheory.WittVector.Identities Mathlib.LinearAlgebra.RootSystem.RootPairingCat Mathlib.FieldTheory.Minpoly.Basic Mathlib.LinearAlgebra.ExteriorPower.Basic Mathlib.RingTheory.Bialgebra.TensorProduct Mathlib.RingTheory.Polynomial.Dickson Mathlib.Algebra.MvPolynomial.Expand Mathlib.RepresentationTheory.GroupCohomology.Resolution Mathlib.RingTheory.Localization.Integral Mathlib.Algebra.Lie.Derivation.Killing Mathlib.RingTheory.AdicCompletion.Exactness Mathlib.RingTheory.Artinian.Module Mathlib.Data.ZMod.Quotient Mathlib.RingTheory.WittVector.Truncated Mathlib.LinearAlgebra.JordanChevalley Mathlib.FieldTheory.ChevalleyWarning Mathlib.LinearAlgebra.QuadraticForm.Basic Mathlib.LinearAlgebra.QuadraticForm.Basis Mathlib.RepresentationTheory.Rep Mathlib.AlgebraicGeometry.EllipticCurve.Affine Mathlib.AlgebraicGeometry.EllipticCurve.Group Mathlib.RingTheory.RingHom.StandardSmooth Mathlib.Algebra.Module.Presentation.Differentials Mathlib.Algebra.CubicDiscriminant Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat Mathlib.RingTheory.Ideal.MinimalPrime Mathlib.GroupTheory.Nilpotent Mathlib.RingTheory.Bialgebra.Basic Mathlib.RingTheory.WittVector.WittPolynomial Mathlib.Algebra.Lie.Free Mathlib.LinearAlgebra.BilinearForm.Orthogonal Mathlib.RingTheory.Polynomial.IrreducibleRing Mathlib.RingTheory.RingHom.Finite Mathlib.RingTheory.AlgebraicIndependent.Defs Mathlib.RingTheory.EssentialFiniteness Mathlib.FieldTheory.IntermediateField.Algebraic Mathlib.Algebra.GCDMonoid.IntegrallyClosed Mathlib.LinearAlgebra.PerfectPairing Mathlib.NumberTheory.DirichletCharacter.Orthogonality Mathlib.RingTheory.MvPolynomial.Symmetric.Defs Mathlib.RingTheory.PowerSeries.Derivative Mathlib.Algebra.Central.Defs Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap Mathlib.RingTheory.Ideal.Cotangent Mathlib.GroupTheory.SchurZassenhaus Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly Mathlib.LinearAlgebra.Trace Mathlib.RingTheory.Polynomial.Radical Mathlib.LinearAlgebra.FreeModule.PID Mathlib.Algebra.Vertex.HVertexOperator Mathlib.Algebra.Lie.IdealOperations Mathlib.Algebra.Algebra.Subalgebra.Rank Mathlib.LinearAlgebra.Matrix.FiniteDimensional Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities Mathlib.RingTheory.Adjoin.Field Mathlib.RingTheory.Derivation.Basic Mathlib.FieldTheory.Finite.Basic Mathlib.Algebra.Polynomial.RingDivision Mathlib.Algebra.Category.ModuleCat.Simple Mathlib.RingTheory.DualNumber Mathlib.Algebra.Lie.TraceForm Mathlib.Algebra.Algebra.Subalgebra.Prod Mathlib.LinearAlgebra.RootSystem.OfBilinear Mathlib.LinearAlgebra.Matrix.Ideal Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf Mathlib.FieldTheory.SplittingField.IsSplittingField Mathlib.Algebra.Polynomial.Taylor Mathlib.Algebra.Lie.Killing Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs Mathlib.Algebra.Lie.Derivation.AdjointAction Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal Mathlib.RingTheory.Polynomial.IntegralNormalization Mathlib.RingTheory.Algebraic.Basic Mathlib.RingTheory.Noetherian.Nilpotent Mathlib.RingTheory.RootsOfUnity.Lemmas Mathlib.Algebra.Lie.Character Mathlib.RingTheory.Presentation Mathlib.Algebra.Lie.DirectSum Mathlib.RingTheory.MvPolynomial.Homogeneous Mathlib.Algebra.Category.Ring.Epi Mathlib.Algebra.Category.ModuleCat.Pseudofunctor Mathlib.Algebra.Polynomial.Expand Mathlib.RingTheory.FractionalIdeal.Basic Mathlib.FieldTheory.Finite.Polynomial Mathlib.LinearAlgebra.FiniteDimensional Mathlib.RingTheory.MvPolynomial.Ideal Mathlib.RingTheory.Polynomial.Vieta Mathlib.RingTheory.Kaehler.CotangentComplex Mathlib.LinearAlgebra.Orientation Mathlib.LinearAlgebra.FreeModule.Int Mathlib.Algebra.DirectSum.Internal Mathlib.RingTheory.Derivation.ToSquareZero Mathlib.NumberTheory.SumFourSquares Mathlib.LinearAlgebra.RootSystem.WeylGroup Mathlib.LinearAlgebra.Matrix.ToLin Mathlib.RingTheory.PowerSeries.PiTopology Mathlib.RingTheory.FinitePresentation Mathlib.Algebra.DirectSum.Idempotents Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal Mathlib.LinearAlgebra.Semisimple Mathlib.LinearAlgebra.RootSystem.Basic Mathlib.RingTheory.Finiteness.Subalgebra Mathlib.Algebra.Lie.Weights.Basic Mathlib.Algebra.Lie.Weights.RootSystem Mathlib.RingTheory.DividedPowers.Basic Mathlib.Algebra.Algebra.Subalgebra.Order Mathlib.RepresentationTheory.Invariants Mathlib.RingTheory.Valuation.Integral Mathlib.RingTheory.RingHom.Injective Mathlib.RingTheory.Ideal.Quotient.Nilpotent Mathlib.RingTheory.MvPolynomial.Localization Mathlib.RingTheory.Localization.LocalizationLocalization Mathlib.RingTheory.Unramified.Pi Mathlib.LinearAlgebra.TensorAlgebra.Basic Mathlib.RingTheory.Localization.Submodule Mathlib.Algebra.Lie.LieTheorem Mathlib.LinearAlgebra.TensorAlgebra.Basis Mathlib.CategoryTheory.Preadditive.Schur Mathlib.RingTheory.Generators Mathlib.RingTheory.Adjoin.Tower Mathlib.Data.Complex.Determinant Mathlib.RingTheory.PolynomialAlgebra Mathlib.RingTheory.Polynomial.HilbertPoly Mathlib.LinearAlgebra.BilinearForm.Properties Mathlib.RingTheory.MvPolynomial.FreeCommRing Mathlib.LinearAlgebra.FiniteDimensional.Defs Mathlib.RingTheory.Nilpotent.Lemmas Mathlib.RingTheory.Jacobson.Ideal Mathlib.RingTheory.Polynomial.Bernstein Mathlib.Algebra.LinearRecurrence Mathlib.LinearAlgebra.TensorProduct.Subalgebra Mathlib.LinearAlgebra.CliffordAlgebra.Star Mathlib.LinearAlgebra.Projectivization.Constructions Mathlib.RingTheory.DiscreteValuationRing.TFAE Mathlib.Algebra.MvPolynomial.Rename Mathlib.NumberTheory.MulChar.Duality Mathlib.RingTheory.ZMod Mathlib.LinearAlgebra.Matrix.Nondegenerate Mathlib.RingTheory.Etale.Kaehler Mathlib.NumberTheory.LegendreSymbol.Basic Mathlib.RingTheory.Adjoin.FG Mathlib.Dynamics.Newton Mathlib.RingTheory.FiniteStability Mathlib.RingTheory.Localization.InvSubmonoid Mathlib.LinearAlgebra.TensorProduct.Matrix Mathlib.Algebra.Algebra.Subalgebra.Pointwise Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic Mathlib.RepresentationTheory.Character Mathlib.RingTheory.RingHom.FinitePresentation Mathlib.Algebra.MvPolynomial.Derivation Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower Mathlib.Algebra.CharP.Subring Mathlib.LinearAlgebra.CliffordAlgebra.Equivs Mathlib.Algebra.MvPolynomial.Variables Mathlib.RepresentationTheory.Basic Mathlib.RingTheory.WittVector.Verschiebung Mathlib.RingTheory.Filtration Mathlib.Algebra.Lie.SkewAdjoint Mathlib.RingTheory.Nakayama Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic Mathlib.LinearAlgebra.CliffordAlgebra.Fold Mathlib.LinearAlgebra.FreeModule.Finite.Matrix Mathlib.LinearAlgebra.Matrix.Charpoly.Basic Mathlib.Algebra.Lie.Weights.Chain Mathlib.Algebra.Polynomial.Derivation Mathlib.RingTheory.Algebraic.Integral Mathlib.RingTheory.Valuation.RamificationGroup Mathlib.RingTheory.MvPolynomial Mathlib.Algebra.Lie.Matrix Mathlib.Algebra.MvPolynomial.Supported Mathlib.RingTheory.MvPolynomial.Tower Mathlib.Data.Matrix.Rank Mathlib.GroupTheory.Torsion Mathlib.Analysis.Convex.Between Mathlib.Algebra.AlgebraicCard Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic Mathlib.LinearAlgebra.Contraction Mathlib.RingTheory.MvPolynomial.EulerIdentity Mathlib.LinearAlgebra.Matrix.BilinearForm Mathlib.RingTheory.Binomial Mathlib.RingTheory.Polynomial.Chebyshev Mathlib.RingTheory.RingHom.Integral Mathlib.RingTheory.Smooth.Basic Mathlib.LinearAlgebra.CliffordAlgebra.Even Mathlib.Algebra.Polynomial.Laurent Mathlib.LinearAlgebra.Multilinear.FiniteDimensional Mathlib.Topology.Algebra.MvPolynomial Mathlib.Algebra.Polynomial.Module.Basic Mathlib.RingTheory.MvPolynomial.Groebner Mathlib.Algebra.Lie.Semisimple.Defs Mathlib.Algebra.Polynomial.Degree.CardPowDegree Mathlib.LinearAlgebra.Eigenspace.Triangularizable Mathlib.RingTheory.MvPowerSeries.Inverse Mathlib.RingTheory.SurjectiveOnStalks Mathlib.LinearAlgebra.Projectivization.Independence Mathlib.LinearAlgebra.Matrix.BaseChange Mathlib.RingTheory.LocalProperties.Exactness Mathlib.Algebra.Category.BialgebraCat.Basic Mathlib.Algebra.MvPolynomial.SchwartzZippel Mathlib.RingTheory.Valuation.LocalSubring Mathlib.RingTheory.Polynomial.Basic Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass Mathlib.Algebra.Lie.Abelian Mathlib.Data.Matrix.Kronecker Mathlib.RingTheory.HopfAlgebra Mathlib.LinearAlgebra.TensorProduct.Submodule Mathlib.Algebra.Algebra.Subalgebra.Basic Mathlib.RingTheory.LocalRing.ResidueField.Defs Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup Mathlib.RingTheory.ReesAlgebra Mathlib.RingTheory.IsTensorProduct Mathlib.Algebra.Module.PID Mathlib.Algebra.MvPolynomial.Comap Mathlib.RingTheory.Ideal.AssociatedPrime Mathlib.RingTheory.Polynomial.GaussLemma Mathlib.LinearAlgebra.CliffordAlgebra.Inversion Mathlib.RingTheory.Polynomial.Wronskian Mathlib.Algebra.Category.AlgebraCat.Symmetric Mathlib.FieldTheory.Finiteness Mathlib.RingTheory.WittVector.StructurePolynomial Mathlib.LinearAlgebra.Dimension.Torsion.Finite Mathlib.LinearAlgebra.FreeAlgebra Mathlib.RingTheory.DedekindDomain.Basic Mathlib.LinearAlgebra.Matrix.Charpoly.Univ Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber Mathlib.GroupTheory.SpecificGroups.Quaternion Mathlib.RingTheory.LocalRing.Subring Mathlib.RingTheory.Extension Mathlib.FieldTheory.Perfect Mathlib.LinearAlgebra.TensorProduct.Graded.External Mathlib.Algebra.Category.FGModuleCat.Basic Mathlib.RingTheory.Algebraic.Pi Mathlib.RingTheory.Localization.Free Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator Mathlib.Algebra.Algebra.Subalgebra.MulOpposite Mathlib.AlgebraicGeometry.EllipticCurve.Projective Mathlib.Topology.Algebra.Algebra Mathlib.Algebra.Module.Torsion Mathlib.Topology.Instances.Matrix Mathlib.Algebra.Jordan.Basic Mathlib.Algebra.Polynomial.GroupRingAction Mathlib.RingTheory.HahnSeries.Valuation Mathlib.RingTheory.Adjoin.Polynomial Mathlib.RingTheory.LocalRing.ResidueField.Basic Mathlib.LinearAlgebra.CliffordAlgebra.Grading Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic Mathlib.RingTheory.Polynomial.SeparableDegree Mathlib.RingTheory.KrullDimension.Basic Mathlib.FieldTheory.Separable Mathlib.LinearAlgebra.TensorProduct.Opposite Mathlib.RingTheory.HahnSeries.Summable Mathlib.FieldTheory.MvRatFunc.Rank Mathlib.Algebra.Module.FinitePresentation Mathlib.RingTheory.AlgebraicIndependent.Basic Mathlib.NumberTheory.KummerDedekind Mathlib.RingTheory.EisensteinCriterion Mathlib.Algebra.Star.Free Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity Mathlib.Algebra.MvPolynomial.Monad Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization Mathlib.RingTheory.Smooth.StandardSmooth Mathlib.LinearAlgebra.CliffordAlgebra.Basic Mathlib.FieldTheory.IsAlgClosed.Spectrum Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits Mathlib.RingTheory.WittVector.Frobenius Mathlib.LinearAlgebra.Vandermonde Mathlib.LinearAlgebra.Matrix.SesquilinearForm Mathlib.LinearAlgebra.Projectivization.Cardinality Mathlib.NumberTheory.Pell Mathlib.Algebra.Category.AlgebraCat.Monoidal Mathlib.LinearAlgebra.CliffordAlgebra.CategoryTheory Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous Mathlib.RingTheory.IntegralClosure.IntegrallyClosed Mathlib.RingTheory.SimpleRing.Matrix Mathlib.RingTheory.WittVector.Basic Mathlib.RingTheory.Jacobson.Ring Mathlib.Tactic.ReduceModChar Mathlib.GroupTheory.Transfer Mathlib.RingTheory.HahnSeries.PowerSeries Mathlib.RepresentationTheory.GroupCohomology.Basic Mathlib.AlgebraicGeometry.PrimeSpectrum.Polynomial Mathlib.RingTheory.Smooth.Kaehler Mathlib.RingTheory.RingHom.Locally Mathlib.RepresentationTheory.FDRep Mathlib.Algebra.MvPolynomial.Equiv Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed Mathlib.Algebra.Polynomial.SumIteratedDerivative Mathlib.RingTheory.Polynomial.Nilpotent Mathlib.CategoryTheory.Monoidal.Internal.Module Mathlib.RingTheory.Unramified.Basic Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv Mathlib.LinearAlgebra.Reflection Mathlib.RingTheory.Adjoin.Dimension Mathlib.LinearAlgebra.AnnihilatingPolynomial Mathlib.RingTheory.Polynomial.UniqueFactorization Mathlib.RingTheory.LocalProperties.Submodule Mathlib.RingTheory.Valuation.AlgebraInstances Mathlib.NumberTheory.FermatPsp Mathlib.RingTheory.Kaehler.Basic Mathlib.GroupTheory.Sylow Mathlib.Algebra.Module.Presentation.Finite Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField Mathlib.RingTheory.MvPowerSeries.Order Mathlib.Algebra.Lie.Semisimple.Basic Mathlib.RingTheory.MvPolynomial.MonomialOrder Mathlib.RingTheory.LocalProperties.Reduced Mathlib.RingTheory.MatrixAlgebra Mathlib.LinearAlgebra.Dimension.LinearMap Mathlib.Algebra.Lie.Derivation.Basic Mathlib.Algebra.Category.AlgebraCat.Basic Mathlib.RingTheory.AdjoinRoot Mathlib.RingTheory.Adjoin.Basic Mathlib.RingTheory.GradedAlgebra.Radical Mathlib.Algebra.Lie.Weights.Killing Mathlib.Algebra.Category.ModuleCat.Presheaf Mathlib.LinearAlgebra.Matrix.ProjectiveSpecialLinearGroup Mathlib.RingTheory.GradedAlgebra.Basic Mathlib.RingTheory.Idempotents Mathlib.RingTheory.Valuation.ValuationSubring Mathlib.RingTheory.Smooth.Pi Mathlib.RingTheory.LocalProperties.IntegrallyClosed Mathlib.Algebra.MvPolynomial.Cardinal Mathlib.Algebra.MvPolynomial.Division Mathlib.RingTheory.Complex Mathlib.LinearAlgebra.Matrix.Adjugate Mathlib.Data.Complex.Module Mathlib.RingTheory.Etale.Pi Mathlib.FieldTheory.KummerExtension Mathlib.NumberTheory.LucasPrimality Mathlib.Algebra.Algebra.Subalgebra.IsSimpleOrder Mathlib.LinearAlgebra.QuadraticForm.Isometry Mathlib.RingTheory.Jacobson.Polynomial Mathlib.ModelTheory.Algebra.Ring.FreeCommRing Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition Mathlib.Algebra.Category.Ring.Under.Basic Mathlib.FieldTheory.Minpoly.Field Mathlib.Topology.Algebra.Module.Determinant Mathlib.SetTheory.Cardinal.Free Mathlib.Algebra.Module.LinearMap.Polynomial Mathlib.NumberTheory.BernoulliPolynomials Mathlib.RepresentationTheory.GroupCohomology.LowDegree Mathlib.Algebra.MonoidAlgebra.Grading Mathlib.RingTheory.RingHomProperties Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear Mathlib.LinearAlgebra.BilinearForm.TensorProduct Mathlib.RingTheory.TensorProduct.Pi Mathlib.RingTheory.AdicCompletion.Algebra Mathlib.Algebra.FreeAlgebra.Cardinality Mathlib.RingTheory.Valuation.Quotient Mathlib.Algebra.Category.Ring.Constructions Mathlib.RingTheory.Polynomial.Eisenstein.Basic Mathlib.Algebra.CharP.LinearMaps Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian Mathlib.Algebra.Lie.BaseChange Mathlib.LinearAlgebra.Dual Mathlib.LinearAlgebra.TensorProduct.RightExactness Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv Mathlib.Algebra.Lie.CartanMatrix Mathlib.Algebra.Central.Basic Mathlib.LinearAlgebra.Matrix.Basis Mathlib.RingTheory.Bialgebra.Equiv Mathlib.Algebra.Polynomial.Lifts Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange Mathlib.GroupTheory.FiniteAbelian.Duality Mathlib.RingTheory.Polynomial.ScaleRoots Mathlib.RingTheory.FractionalIdeal.Operations Mathlib.LinearAlgebra.QuadraticForm.TensorProduct Mathlib.RingTheory.Etale.Basic Mathlib.Algebra.Lie.UniversalEnveloping Mathlib.LinearAlgebra.Dimension.Torsion.Basic Mathlib.ModelTheory.Algebra.Field.CharP Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange Mathlib.RingTheory.WittVector.Teichmuller Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono Mathlib.LinearAlgebra.CliffordAlgebra.Contraction Mathlib.Algebra.CharP.Algebra Mathlib.Algebra.Lie.Subalgebra Mathlib.RingTheory.MvPolynomial.Basic Mathlib.Algebra.MvPolynomial.PDeriv Mathlib.RingTheory.FreeCommRing Mathlib.RingTheory.PowerSeries.Order Mathlib.Algebra.MvPolynomial.CommRing Mathlib.Algebra.Polynomial.Module.FiniteDimensional Mathlib.CategoryTheory.Preadditive.HomOrthogonal Mathlib.Analysis.Convex.Visible Mathlib.RingTheory.WittVector.IsPoly Mathlib.RingTheory.Kaehler.TensorProduct Mathlib.LinearAlgebra.Dimension.Constructions Mathlib.RingTheory.LocalProperties.Basic Mathlib.LinearAlgebra.Dimension.ErdosKaplansky Mathlib.Algebra.Lie.Solvable Mathlib.GroupTheory.SpecificGroups.Cyclic Mathlib.RingTheory.Ideal.Quotient.Operations Mathlib.Algebra.Lie.Weights.Cartan Mathlib.RingTheory.Artinian.Instances Mathlib.NumberTheory.Bernoulli Mathlib.LinearAlgebra.SymplecticGroup Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ Mathlib.LinearAlgebra.Determinant Mathlib.RingTheory.LocalRing.RingHom.Basic Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card Mathlib.RingTheory.WittVector.Defs Mathlib.Algebra.Central.Matrix Mathlib.RingTheory.FiniteLength Mathlib.Algebra.MvPolynomial.Polynomial Mathlib.GroupTheory.FiniteAbelian.Basic Mathlib.RingTheory.IntegralClosure.Algebra.Basic Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree Mathlib.LinearAlgebra.AffineSpace.Matrix Mathlib.GroupTheory.Order.Min Mathlib.FieldTheory.PerfectClosure Mathlib.LinearAlgebra.CliffordAlgebra.Prod Mathlib.LinearAlgebra.Eigenspace.Pi Mathlib.Algebra.Lie.Classical Mathlib.RingTheory.MvPowerSeries.Trunc Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries Mathlib.Algebra.Polynomial.Bivariate Mathlib.RingTheory.DedekindDomain.Factorization Mathlib.RingTheory.MvPowerSeries.Basic Mathlib.RingTheory.MaximalSpectrum Mathlib.GroupTheory.SpecificGroups.KleinFour Mathlib.Algebra.Polynomial.Roots Mathlib.RingTheory.FiniteType Mathlib.Algebra.CharP.IntermediateField Mathlib.LinearAlgebra.Projectivization.Subspace Mathlib.Data.Complex.Orientation Mathlib.RingTheory.Polynomial.RationalRoot Mathlib.Topology.Algebra.Module.CharacterSpace Mathlib.LinearAlgebra.Matrix.ToLinearEquiv Mathlib.FieldTheory.IntermediateField.Basic Mathlib.Algebra.MvPolynomial.Degrees Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal Mathlib.RingTheory.IntegralDomain Mathlib.RingTheory.RootsOfUnity.Minpoly Mathlib.RingTheory.HahnSeries.Multiplication Mathlib.RingTheory.TensorProduct.Free Mathlib.RingTheory.PrimeSpectrum Mathlib.Algebra.CharP.MixedCharZero Mathlib.GroupTheory.Frattini Mathlib.RingTheory.WittVector.DiscreteValuationRing Mathlib.RingTheory.MvPowerSeries.PiTopology Mathlib.Algebra.MvPolynomial.Invertible Mathlib.GroupTheory.PGroup Mathlib.Algebra.Category.ModuleCat.Presheaf.Abelian Mathlib.RingTheory.RingHom.Surjective Mathlib.NumberTheory.ModularForms.CongruenceSubgroups Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward Mathlib.LinearAlgebra.TensorProduct.Graded.Internal Mathlib.LinearAlgebra.Dimension.Finite Mathlib.RingTheory.DedekindDomain.PID Mathlib.LinearAlgebra.RootSystem.RootPositive Mathlib.LinearAlgebra.Matrix.IsDiag Mathlib.Analysis.Convex.Radon Mathlib.Algebra.Category.Ring.Adjunctions Mathlib.Algebra.Lie.TensorProduct Mathlib.RingTheory.Norm.Transitivity Mathlib.FieldTheory.SplittingField.Construction Mathlib.FieldTheory.RatFunc.Basic Mathlib.LinearAlgebra.Charpoly.BaseChange Mathlib.RingTheory.Support Mathlib.Algebra.Lie.Weights.Linear Mathlib.RepresentationTheory.Maschke Mathlib.RingTheory.Kaehler.JacobiZariski Mathlib.Algebra.Category.HopfAlgebraCat.Basic Mathlib.GroupTheory.Schreier Mathlib.RingTheory.NormTrace Mathlib.RingTheory.Derivation.MapCoeffs Mathlib.RingTheory.TensorProduct.Basic Mathlib.LinearAlgebra.RootSystem.Hom Mathlib.Combinatorics.Additive.CauchyDavenport Mathlib.Algebra.Module.GradedModule Mathlib.LinearAlgebra.Dimension.RankNullity Mathlib.LinearAlgebra.Basis.Flag Mathlib.LinearAlgebra.Matrix.NonsingularInverse Mathlib.Algebra.Lie.InvariantForm Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic Mathlib.RingTheory.RootsOfUnity.Basic Mathlib.RingTheory.Localization.Away.AdjoinRoot Mathlib.Algebra.Polynomial.Module.AEval Mathlib.NumberTheory.FLT.MasonStothers Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings Mathlib.Algebra.FreeAlgebra Mathlib.RingTheory.PowerSeries.Trunc Mathlib.LinearAlgebra.Matrix.FixedDetMatrices Mathlib.LinearAlgebra.ExteriorAlgebra.Basic Mathlib.RingTheory.PowerSeries.Basic Mathlib.RingTheory.TensorProduct.MvPolynomial Mathlib.LinearAlgebra.TensorProduct.Vanishing Mathlib.NumberTheory.FLT.Polynomial Mathlib.Algebra.Polynomial.Smeval Mathlib.RingTheory.Localization.Algebra Mathlib.LinearAlgebra.Matrix.Dual Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors Mathlib.GroupTheory.SpecificGroups.ZGroup Mathlib.RingTheory.LocalProperties.Projective Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic Mathlib.RingTheory.Derivation.DifferentialRing Mathlib.FieldTheory.Differential.Basic Mathlib.Algebra.Lie.OfAssociative Mathlib.Algebra.Colimit.Ring Mathlib.RingTheory.PowerSeries.Inverse Mathlib.LinearAlgebra.QuadraticForm.Dual Mathlib.LinearAlgebra.Matrix.Block Mathlib.LinearAlgebra.FreeProduct.Basic Mathlib.Algebra.Category.ModuleCat.Presheaf.Free Mathlib.LinearAlgebra.RootSystem.Defs Mathlib.LinearAlgebra.Projectivization.Basic Mathlib.RingTheory.WittVector.MulP Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate Mathlib.Data.Nat.Factorial.SuperFactorial
 3
23 files Mathlib.LinearAlgebra.Eigenspace.Matrix Mathlib.Algebra.Lie.Nilpotent Mathlib.Algebra.Star.Subalgebra Mathlib.Algebra.Lie.CartanSubalgebra Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup Mathlib.NumberTheory.PellMatiyasevic Mathlib.NumberTheory.Zsqrtd.GaussianInt Mathlib.Topology.Algebra.StarSubalgebra Mathlib.Algebra.Algebra.Spectrum Mathlib.LinearAlgebra.Eigenspace.Basic Mathlib.Algebra.Lie.EngelSubalgebra Mathlib.NumberTheory.Dioph Mathlib.LinearAlgebra.Eigenspace.Semisimple Mathlib.LinearAlgebra.UnitaryGroup Mathlib.Algebra.Lie.Sl2 Mathlib.Algebra.Lie.Engel Mathlib.Algebra.Lie.Rank Mathlib.NumberTheory.Zsqrtd.Basic Mathlib.LinearAlgebra.Eigenspace.Zero Mathlib.LinearAlgebra.Eigenspace.Minpoly Mathlib.Algebra.Star.Unitary Mathlib.Algebra.Lie.CartanExists Mathlib.Algebra.DirectSum.LinearMap
 4

Declarations diff

+ adjoin_nonUnitalStarSubalgebra_eq_span
+ adjoin_nonUnitalSubalgebra_eq_span
+ coe_toNonUnitalSubsemiring
+ mem_toNonUnitalSubsemiring
+ one_mem_toNonUnitalStarSubalgebra
+ one_mem_toNonUnitalSubalgebra
+ one_mem_toNonUnitalSubring
+ one_mem_toNonUnitalSubsemiring
+ subsemiringClosure_toNonUnitalSubsemiring
+ toNonUnitalStarSubalgebra
+ toNonUnitalSubalgebra
+ toNonUnitalSubring
+ toNonUnitalSubsemiring
+ toNonUnitalSubsemiring_inj
+ toNonUnitalSubsemiring_injective
- Algebra.adjoin_nonUnitalSubalgebra_eq_span
- StarAlgebra.adjoin_nonUnitalStarSubalgebra_eq_span
- StarSubalgebra.one_mem_toNonUnitalStarSubalgebra
- StarSubalgebra.toNonUnitalStarSubalgebra
- Subalgebra.one_mem_toNonUnitalSubalgebra
- Subalgebra.toNonUnitalSubalgebra
- Submonoid.subsemiringClosure_toNonUnitalSubsemiring
- Subring.one_mem_toNonUnitalSubring
- Subring.toNonUnitalSubring
- Subsemiring.coe_toNonUnitalSubsemiring
- Subsemiring.mem_toNonUnitalSubsemiring
- Subsemiring.one_mem_toNonUnitalSubsemiring
- Subsemiring.toNonUnitalSubsemiring
- Subsemiring.toNonUnitalSubsemiring_inj
- Subsemiring.toNonUnitalSubsemiring_injective

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

@github-actions github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Jan 6, 2025
@YaelDillies YaelDillies mentioned this pull request Jan 6, 2025
Open
7 tasks
@artie2000
Copy link
Collaborator

artie2000 commented Jan 6, 2025 •
edited
Loading

What happened to NonUnitalSubsemiring.toSubsemiring, NonUnitalSubsemiring.toSubsemiring_toNonUnitalSubsemiring, and Subsemiring.toNonUnitalSubsemiring_toSubsemiring?

@YaelDillies
Copy link
Collaborator Author

What happened to NonUnitalSubsemiring.toSubsemiring, NonUnitalSubsemiring.toSubsemiring_toNonUnitalSubsemiring, and Subsemiring.toNonUnitalSubsemiring_toSubsemiring?

🫥. They are now back

artie2000
artie2000 approved these changes Jan 8, 2025
View reviewed changes
Copy link
Collaborator

@artie2000 artie2000 left a comment

Choose a reason for hiding this comment

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

LGTM

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

@artie2000 artie2000 artie2000 approved these changes

Assignees
No one assigned
Labels
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
@YaelDillies @artie2000 @eric-wieser