[Merged by Bors] - chore(Noetherian/Artinian): generalize to Semiring#20534
Closed
alreadydone wants to merge 3 commits intomasterfrom
Closed
[Merged by Bors] - chore(Noetherian/Artinian): generalize to Semiring#20534alreadydone wants to merge 3 commits intomasterfrom
alreadydone wants to merge 3 commits intomasterfrom
Conversation
Contributor
alreadydone
commented
Jan 7, 2025
PR summary 2083001ee0
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.RingTheory.Noetherian.Basic | 1063 | 1064 | +1 (+0.09%) |
| Mathlib.RingTheory.Artinian.Module | 1096 | 1097 | +1 (+0.09%) |
| Mathlib.RingTheory.Artinian.Ring | 1112 | 1113 | +1 (+0.09%) |
| Mathlib.RingTheory.SimpleModule | 1149 | 1150 | +1 (+0.09%) |
Import changes for all files
| Files | Import difference |
|---|---|
927 filesMathlib.LinearAlgebra.FreeModule.Norm Mathlib.LinearAlgebra.Charpoly.Basic Mathlib.NumberTheory.NumberField.Discriminant.Defs Mathlib.MeasureTheory.Integral.VitaliCaratheodory Mathlib.Topology.Algebra.Module.Simple Mathlib.Combinatorics.Additive.ErdosGinzburgZiv Mathlib.RingTheory.IsAdjoinRoot Mathlib.Analysis.BoxIntegral.UnitPartition Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs Mathlib.Analysis.CStarAlgebra.GelfandDuality Mathlib.Probability.Process.HittingTime Mathlib.Analysis.InnerProductSpace.Spectrum Mathlib.Analysis.InnerProductSpace.Symmetric Mathlib.Analysis.InnerProductSpace.OfNorm Mathlib.RingTheory.DedekindDomain.Dvr Mathlib.RingTheory.Henselian Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Symmetric Mathlib.FieldTheory.IsPerfectClosure Mathlib.Probability.BorelCantelli Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv Mathlib.NumberTheory.Wilson Mathlib.Geometry.Manifold.ContMDiff.Atlas Mathlib.RepresentationTheory.GroupCohomology.Hilbert90 Mathlib.NumberTheory.LSeries.HurwitzZetaValues Mathlib.RingTheory.PowerBasis Mathlib.Algebra.Symmetrized Mathlib.Algebra.Lie.Normalizer Mathlib.Analysis.SpecialFunctions.Gamma.Basic Mathlib.Geometry.Manifold.VectorBundle.Pullback Mathlib.FieldTheory.Finite.Trace Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual Mathlib.LinearAlgebra.Matrix.ZPow Mathlib.Analysis.Convex.AmpleSet Mathlib.Probability.Variance Mathlib.RingTheory.Noetherian.Orzech Mathlib.Analysis.Complex.Angle Mathlib.LinearAlgebra.Matrix.PosDef Mathlib.RingTheory.SimpleModule Mathlib.Algebra.Category.FGModuleCat.Limits Mathlib.Analysis.SpecialFunctions.Integrals Mathlib.NumberTheory.Harmonic.ZetaAsymp Mathlib.Dynamics.Ergodic.AddCircle Mathlib.Analysis.Calculus.BumpFunction.Convolution Mathlib.Analysis.Fourier.PoissonSummation Mathlib.Analysis.InnerProductSpace.Rayleigh Mathlib.Analysis.Normed.Module.Dual Mathlib.LinearAlgebra.ExteriorAlgebra.Grading Mathlib.Geometry.Manifold.VectorBundle.Basic Mathlib.Analysis.Calculus.Deriv.Abs Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds Mathlib.MeasureTheory.Measure.FiniteMeasure Mathlib.Tactic.FunProp.ContDiff Mathlib.MeasureTheory.Integral.IntervalAverage Mathlib.Analysis.Distribution.FourierSchwartz Mathlib.RingTheory.WittVector.Domain Mathlib.Analysis.Calculus.ParametricIntervalIntegral Mathlib.MeasureTheory.Measure.ProbabilityMeasure Mathlib.Geometry.Manifold.VectorBundle.Tangent Mathlib.MeasureTheory.Function.UnifTight Mathlib.Algebra.Lie.Quotient Mathlib.RingTheory.AlgebraicIndependent.Transcendental Mathlib.Geometry.Manifold.Diffeomorph Mathlib.LinearAlgebra.Dimension.DivisionRing Mathlib.LinearAlgebra.FreeModule.StrongRankCondition Mathlib.MeasureTheory.Measure.Lebesgue.Complex Mathlib.LinearAlgebra.BilinearForm.DualLattice Mathlib.NumberTheory.EulerProduct.DirichletLSeries Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology Mathlib.MeasureTheory.Integral.IntervalIntegral Mathlib.Analysis.Complex.AbsMax Mathlib.RingTheory.Ideal.Over Mathlib.RingTheory.GradedAlgebra.Noetherian Mathlib.Analysis.InnerProductSpace.ProdL2 Mathlib.Probability.Kernel.Disintegration.CDFToKernel Mathlib.RingTheory.LocalRing.Quotient Mathlib.Algebra.Category.ModuleCat.Differentials.Basic Mathlib.Data.Real.GoldenRatio Mathlib.RingTheory.WittVector.InitTail Mathlib.Geometry.Manifold.MFDeriv.Basic Mathlib.Analysis.CStarAlgebra.Spectrum Mathlib.LinearAlgebra.Dimension.Localization Mathlib.Geometry.Manifold.Instances.Real Mathlib.RingTheory.Localization.NormTrace Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv Mathlib.LinearAlgebra.Lagrange Mathlib.Geometry.Manifold.Complex Mathlib.LinearAlgebra.Coevaluation Mathlib.Algebra.Lie.Submodule Mathlib.FieldTheory.AbelRuffini Mathlib.MeasureTheory.Integral.CircleIntegral Mathlib.Probability.StrongLaw Mathlib.RingTheory.Regular.RegularSequence Mathlib.Analysis.Normed.Module.FiniteDimension Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique Mathlib.LinearAlgebra.Matrix.Diagonal Mathlib.RingTheory.Derivation.Lie Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral Mathlib.RingTheory.Algebraic.MvPolynomial Mathlib.Probability.Kernel.Composition.MeasureCompProd Mathlib.RingTheory.Trace.Defs Mathlib.RingTheory.WittVector.Compare Mathlib.Probability.Kernel.Composition.IntegralCompProd Mathlib.LinearAlgebra.Eigenspace.Matrix 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.MeasureTheory.Measure.LevyProkhorovMetric Mathlib.RingTheory.Polynomial.Quotient Mathlib.Algebra.Module.ZLattice.Covolume Mathlib.LinearAlgebra.PID Mathlib.NumberTheory.ModularForms.Identities Mathlib.MeasureTheory.Function.ContinuousMapDense Mathlib.Analysis.Complex.Periodic Mathlib.Geometry.Manifold.ContMDiffMap Mathlib.Algebra.MvPolynomial.Funext Mathlib.NumberTheory.NumberField.Norm Mathlib.Topology.Category.Profinite.Nobeling Mathlib.LinearAlgebra.FreeModule.Determinant Mathlib.FieldTheory.Isaacs Mathlib.Analysis.Complex.TaylorSeries Mathlib.Analysis.Normed.Algebra.Spectrum Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions Mathlib.RingTheory.LocalRing.ResidueField.Ideal Mathlib.Topology.Compactification.OnePointEquiv Mathlib.Analysis.FunctionalSpaces.SobolevInequality Mathlib.LinearAlgebra.QuadraticForm.Prod Mathlib.RingTheory.Trace.Basic Mathlib.Analysis.CStarAlgebra.Module.Constructions Mathlib.Probability.Distributions.Exponential Mathlib.RingTheory.WittVector.MulCoeff Mathlib.RingTheory.RingHom.FiniteType Mathlib.RingTheory.Artinian.Ring Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric Mathlib.Analysis.SpecialFunctions.Complex.Arctan Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation Mathlib.Algebra.Lie.Nilpotent Mathlib.Analysis.BoxIntegral.Partition.Measure Mathlib.LinearAlgebra.Charpoly.ToMatrix Mathlib.RingTheory.Ideal.Quotient.Noetherian Mathlib.FieldTheory.Normal Mathlib.GroupTheory.FreeAbelianGroupFinsupp Mathlib.LinearAlgebra.FreeModule.IdealQuotient Mathlib.Analysis.Fourier.AddCircleMulti Mathlib.Probability.Martingale.Upcrossing Mathlib.MeasureTheory.Function.SimpleFuncDenseLp Mathlib.Analysis.RCLike.Lemmas Mathlib.Algebra.Quaternion Mathlib.Data.Nat.Choose.Lucas Mathlib.Probability.Martingale.OptionalSampling Mathlib.RingTheory.Norm.Defs Mathlib.RingTheory.Kaehler.Polynomial Mathlib.Analysis.RCLike.Inner Mathlib.RingTheory.WittVector.Identities Mathlib.Analysis.Convex.GaugeRescale Mathlib.LinearAlgebra.RootSystem.RootPairingCat Mathlib.FieldTheory.Minpoly.Basic Mathlib.FieldTheory.Adjoin Mathlib.MeasureTheory.Integral.DivergenceTheorem Mathlib.LinearAlgebra.ExteriorPower.Basic Mathlib.Analysis.SpecialFunctions.Log.NegMulLog Mathlib.Analysis.Calculus.BumpFunction.Basic Mathlib.RepresentationTheory.GroupCohomology.Resolution Mathlib.LinearAlgebra.Matrix.Gershgorin Mathlib.Algebra.DualQuaternion Mathlib.RingTheory.Localization.Integral Mathlib.Algebra.Lie.Derivation.Killing Mathlib.RingTheory.AdicCompletion.Exactness Mathlib.MeasureTheory.Measure.LogLikelihoodRatio Mathlib.FieldTheory.SeparableClosure Mathlib.RingTheory.Artinian.Module Mathlib.RingTheory.WittVector.Truncated Mathlib.NumberTheory.SiegelsLemma Mathlib.LinearAlgebra.JordanChevalley Mathlib.Analysis.SpecialFunctions.ImproperIntegrals 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.RepresentationTheory.Rep Mathlib.AlgebraicGeometry.EllipticCurve.Affine Mathlib.RingTheory.RingHom.StandardSmooth Mathlib.Algebra.Module.Presentation.Differentials 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.NumberTheory.ModularForms.JacobiTheta.Manifold Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff Mathlib.Algebra.Lie.Free Mathlib.Analysis.InnerProductSpace.NormPow Mathlib.Algebra.Module.ZLattice.Basic Mathlib.Analysis.Convex.Intrinsic Mathlib.LinearAlgebra.BilinearForm.Orthogonal Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls Mathlib.RingTheory.Invariant Mathlib.MeasureTheory.Integral.FundThmCalculus Mathlib.Probability.Kernel.Disintegration.Integral Mathlib.NumberTheory.LSeries.HurwitzZetaEven Mathlib.RingTheory.Unramified.Field Mathlib.Analysis.CStarAlgebra.Matrix Mathlib.RingTheory.EssentialFiniteness Mathlib.FieldTheory.IntermediateField.Algebraic Mathlib.Algebra.GCDMonoid.IntegrallyClosed Mathlib.LinearAlgebra.PerfectPairing Mathlib.FieldTheory.SeparableDegree Mathlib.Geometry.Manifold.PoincareConjecture Mathlib.FieldTheory.Minpoly.MinpolyDiv Mathlib.MeasureTheory.Measure.Portmanteau Mathlib.NumberTheory.LSeries.Deriv Mathlib.MeasureTheory.Measure.Haar.NormedSpace Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap Mathlib.RingTheory.Ideal.Cotangent Mathlib.Analysis.Fourier.AddCircle Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar Mathlib.Analysis.Calculus.MeanValue Mathlib.Analysis.Calculus.LineDeriv.QuadraticMap Mathlib.Analysis.Fourier.Inversion Mathlib.Analysis.Normed.Algebra.QuaternionExponential Mathlib.Computability.AkraBazzi.AkraBazzi Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly Mathlib.Algebra.Lie.CartanSubalgebra Mathlib.LinearAlgebra.Trace Mathlib.LinearAlgebra.FreeModule.PID Mathlib.Algebra.Lie.IdealOperations Mathlib.Algebra.Algebra.Subalgebra.Rank Mathlib.NumberTheory.NumberField.Completion Mathlib.Probability.Kernel.WithDensity Mathlib.Analysis.SpecialFunctions.NonIntegrable Mathlib.Geometry.Euclidean.Angle.Oriented.Basic Mathlib.FieldTheory.Galois.GaloisClosure Mathlib.LinearAlgebra.Matrix.FiniteDimensional Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable Mathlib.FieldTheory.Fixed Mathlib.RingTheory.Adjoin.Field Mathlib.Geometry.Euclidean.Sphere.Ptolemy Mathlib.FieldTheory.Finite.Basic Mathlib.Topology.Algebra.Module.FiniteDimension Mathlib.Algebra.Category.ModuleCat.Simple 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.NumberTheory.ModularForms.EisensteinSeries.Basic Mathlib.Algebra.Lie.TraceForm Mathlib.Analysis.LocallyConvex.WeakSpace Mathlib.RingTheory.Noetherian.Basic 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.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.Algebra.Lie.Derivation.AdjointAction Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal Mathlib.Probability.Distributions.Gaussian Mathlib.NumberTheory.LSeries.Injectivity Mathlib.Probability.Kernel.CondDistrib Mathlib.RingTheory.Algebraic.Basic Mathlib.Analysis.Calculus.FDeriv.Measurable Mathlib.Analysis.Calculus.UniformLimitsDeriv Mathlib.RingTheory.RootsOfUnity.Lemmas Mathlib.NumberTheory.ModularForms.LevelOne Mathlib.MeasureTheory.Integral.Bochner Mathlib.Algebra.Lie.Character 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.Algebra.Lie.DirectSum Mathlib.Probability.Martingale.Basic Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho Mathlib.Algebra.Polynomial.Expand Mathlib.FieldTheory.Finite.Polynomial Mathlib.Geometry.Manifold.IntegralCurve.Basic Mathlib.LinearAlgebra.FiniteDimensional 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.LinearAlgebra.FreeModule.Int Mathlib.NumberTheory.LSeries.Basic Mathlib.Geometry.Manifold.ContMDiffMFDeriv Mathlib.MeasureTheory.Decomposition.SignedLebesgue Mathlib.NumberTheory.SumFourSquares Mathlib.LinearAlgebra.RootSystem.WeylGroup Mathlib.Combinatorics.Configuration Mathlib.Analysis.Convex.StrictConvexSpace Mathlib.Geometry.Manifold.ContMDiff.Basic Mathlib.MeasureTheory.Measure.WithDensityFinite Mathlib.RingTheory.Etale.Field Mathlib.Geometry.Euclidean.Sphere.Power Mathlib.Data.Real.Pi.Irrational Mathlib.RingTheory.FinitePresentation 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.MeasureTheory.Covering.LiminfLimsup Mathlib.Geometry.Euclidean.Angle.Sphere Mathlib.Analysis.InnerProductSpace.LinearPMap Mathlib.Analysis.Complex.UpperHalfPlane.Topology Mathlib.Analysis.Complex.IsIntegral Mathlib.RepresentationTheory.Invariants Mathlib.RingTheory.Valuation.Integral Mathlib.MeasureTheory.Order.UpperLower Mathlib.NumberTheory.Rayleigh Mathlib.Analysis.Calculus.ParametricIntegral Mathlib.MeasureTheory.Function.AEEqFun.DomAct Mathlib.Probability.Martingale.Convergence Mathlib.FieldTheory.KrullTopology Mathlib.Analysis.Complex.UpperHalfPlane.Metric 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.LinearAlgebra.TensorAlgebra.Basis Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable Mathlib.CategoryTheory.Preadditive.Schur Mathlib.Analysis.InnerProductSpace.Basic Mathlib.RingTheory.Generators Mathlib.RingTheory.Adjoin.Tower 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.Analysis.Calculus.LagrangeMultipliers Mathlib.LinearAlgebra.BilinearForm.Properties Mathlib.Analysis.InnerProductSpace.Completion Mathlib.Analysis.Convex.Integral Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace Mathlib.LinearAlgebra.FiniteDimensional.Defs Mathlib.FieldTheory.Galois.Profinite Mathlib.FieldTheory.LinearDisjoint Mathlib.Algebra.LinearRecurrence Mathlib.LinearAlgebra.CliffordAlgebra.Star Mathlib.LinearAlgebra.Projectivization.Constructions Mathlib.RingTheory.DiscreteValuationRing.TFAE Mathlib.MeasureTheory.Integral.Prod Mathlib.MeasureTheory.Integral.Layercake Mathlib.Geometry.Euclidean.Circumcenter Mathlib.LinearAlgebra.Matrix.Nondegenerate Mathlib.Analysis.CStarAlgebra.Module.Defs Mathlib.Analysis.Complex.Schwarz Mathlib.NumberTheory.LegendreSymbol.Basic Mathlib.RingTheory.Adjoin.FG Mathlib.Analysis.Fourier.FourierTransformDeriv Mathlib.RingTheory.FiniteStability Mathlib.RingTheory.Localization.InvSubmonoid Mathlib.Analysis.Complex.UpperHalfPlane.Manifold Mathlib.LinearAlgebra.TensorProduct.Matrix Mathlib.FieldTheory.Finite.GaloisField Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic Mathlib.RepresentationTheory.Character 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.RepresentationTheory.Basic Mathlib.FieldTheory.Galois.Basic Mathlib.RingTheory.WittVector.Verschiebung Mathlib.RingTheory.Filtration Mathlib.Geometry.Manifold.Algebra.SmoothFunctions Mathlib.Algebra.Lie.SkewAdjoint Mathlib.Geometry.Euclidean.Inversion.Calculus Mathlib.Analysis.Calculus.FirstDerivativeTest Mathlib.LinearAlgebra.LinearDisjoint Mathlib.Analysis.InnerProductSpace.Positive Mathlib.LinearAlgebra.CliffordAlgebra.Fold Mathlib.LinearAlgebra.FreeModule.Finite.Matrix 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.RingTheory.MvPolynomial 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.LinearAlgebra.QuadraticForm.Complex Mathlib.MeasureTheory.Measure.FiniteMeasureProd Mathlib.Geometry.Manifold.Sheaf.Smooth Mathlib.Geometry.Manifold.VectorBundle.Hom Mathlib.Analysis.InnerProductSpace.Orthogonal Mathlib.Probability.Kernel.MeasurableIntegral Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable Mathlib.Geometry.Euclidean.MongePoint Mathlib.Topology.CWComplex Mathlib.Analysis.Convex.Between Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional Mathlib.Algebra.AlgebraicCard Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds Mathlib.Data.Real.Irrational Mathlib.LinearAlgebra.Contraction 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.RingTheory.Smooth.Basic Mathlib.LinearAlgebra.CliffordAlgebra.Even Mathlib.LinearAlgebra.Multilinear.FiniteDimensional Mathlib.Combinatorics.Additive.Randomisation Mathlib.NumberTheory.LSeries.Dirichlet Mathlib.Analysis.InnerProductSpace.Projection Mathlib.NumberTheory.Transcendental.Liouville.Residual Mathlib.MeasureTheory.Integral.Asymptotics Mathlib.Algebra.Lie.Semisimple.Defs 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.Geometry.Euclidean.Angle.Unoriented.Conformal Mathlib.Analysis.Convex.Strong Mathlib.Analysis.SpecialFunctions.BinaryEntropy Mathlib.LinearAlgebra.Projectivization.Independence Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable Mathlib.LinearAlgebra.Matrix.BaseChange Mathlib.Analysis.Fourier.RiemannLebesgueLemma Mathlib.LinearAlgebra.InvariantBasisNumber Mathlib.Analysis.SpecialFunctions.SmoothTransition Mathlib.Data.Complex.FiniteDimensional Mathlib.Analysis.BoxIntegral.Basic Mathlib.Analysis.InnerProductSpace.Orthonormal Mathlib.RingTheory.Polynomial.Basic Mathlib.Analysis.Quaternion Mathlib.Algebra.Lie.Abelian Mathlib.Data.Matrix.Kronecker Mathlib.Analysis.BoxIntegral.Integrability Mathlib.RingTheory.Discriminant Mathlib.NumberTheory.SumTwoSquares Mathlib.Analysis.InnerProductSpace.Calculus Mathlib.Topology.Category.TopCat.Sphere Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup Mathlib.RingTheory.ReesAlgebra Mathlib.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.FieldTheory.Finiteness Mathlib.MeasureTheory.Integral.IntegralEqImproper Mathlib.Analysis.Complex.Polynomial.Basic 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.LinearAlgebra.FreeAlgebra Mathlib.Analysis.Complex.RemovableSingularity Mathlib.RingTheory.DedekindDomain.Basic Mathlib.LinearAlgebra.Matrix.Charpoly.Univ Mathlib.Analysis.Convex.Normed Mathlib.MeasureTheory.Measure.Tilted Mathlib.Analysis.Complex.Liouville Mathlib.RingTheory.AdicCompletion.AsTensorProduct Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber Mathlib.NumberTheory.Transcendental.Liouville.Measure Mathlib.Analysis.Convex.Continuous Mathlib.Analysis.InnerProductSpace.LinearMap Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle Mathlib.NumberTheory.LSeries.MellinEqDirichlet Mathlib.Analysis.InnerProductSpace.MeanErgodic Mathlib.RingTheory.Extension Mathlib.MeasureTheory.Function.Jacobian Mathlib.FieldTheory.Perfect Mathlib.NumberTheory.DiophantineApproximation.ContinuedFractions Mathlib.NumberTheory.Transcendental.Lindemann.Init.AnalyticalPart Mathlib.Analysis.Complex.LocallyUniformLimit Mathlib.FieldTheory.IsAlgClosed.Basic Mathlib.Algebra.Category.FGModuleCat.Basic Mathlib.NumberTheory.LSeries.Positivity Mathlib.FieldTheory.Minpoly.IsConjRoot Mathlib.Analysis.InnerProductSpace.EuclideanDist Mathlib.Analysis.Convex.Measure Mathlib.Probability.Moments Mathlib.NumberTheory.Harmonic.EulerMascheroni Mathlib.RingTheory.Localization.Free Mathlib.Analysis.SpecialFunctions.Log.Deriv Mathlib.LinearAlgebra.Eigenspace.Basic Mathlib.FieldTheory.Cardinality Mathlib.Algebra.Lie.EngelSubalgebra 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.Analysis.Complex.Conformal Mathlib.Topology.Instances.Matrix Mathlib.Topology.Instances.Complex Mathlib.Algebra.Jordan.Basic Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup Mathlib.RingTheory.LocalRing.ResidueField.Basic 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.FieldTheory.MvRatFunc.Rank Mathlib.Algebra.Module.FinitePresentation Mathlib.Geometry.Manifold.MFDeriv.Defs Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional 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.RingTheory.WittVector.Frobenius Mathlib.Analysis.Calculus.LineDeriv.Measurable Mathlib.LinearAlgebra.Vandermonde Mathlib.LinearAlgebra.Matrix.SesquilinearForm Mathlib.LinearAlgebra.Projectivization.Cardinality Mathlib.NumberTheory.Pell 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.RingTheory.Jacobson.Ring Mathlib.Tactic.ReduceModChar Mathlib.MeasureTheory.Integral.BoundedContinuousFunction Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty Mathlib.RepresentationTheory.GroupCohomology.Basic Mathlib.RingTheory.Smooth.Kaehler Mathlib.Geometry.Manifold.ContMDiff.Defs Mathlib.Analysis.Normed.Algebra.Basic Mathlib.MeasureTheory.Integral.ExpDecay Mathlib.RepresentationTheory.FDRep Mathlib.Dynamics.Ergodic.Action.OfMinimal Mathlib.RingTheory.WittVector.Isocrystal Mathlib.Geometry.Manifold.IntegralCurve.UniformTime 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.RingTheory.Adjoin.Dimension Mathlib.LinearAlgebra.AnnihilatingPolynomial Mathlib.RingTheory.Polynomial.UniqueFactorization Mathlib.MeasureTheory.Constructions.HaarToSphere Mathlib.Analysis.SpecialFunctions.JapaneseBracket Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField Mathlib.MeasureTheory.Integral.CircleTransform Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent Mathlib.NumberTheory.FermatPsp Mathlib.RingTheory.Kaehler.Basic Mathlib.MeasureTheory.Integral.DominatedConvergence Mathlib.Algebra.Module.Presentation.Finite Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField Mathlib.NumberTheory.ZetaValues Mathlib.Analysis.Convex.Deriv Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine Mathlib.Analysis.SpecialFunctions.Arsinh Mathlib.Analysis.Complex.Positivity Mathlib.Analysis.Calculus.ContDiff.FiniteDimension Mathlib.Algebra.Lie.Semisimple.Basic Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure Mathlib.Analysis.Fourier.FourierTransform Mathlib.LinearAlgebra.Dimension.LinearMap Mathlib.Algebra.Lie.Derivation.Basic 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.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.LinearAlgebra.Matrix.Adjugate Mathlib.LinearAlgebra.Matrix.SchurComplement Mathlib.RingTheory.Etale.Pi Mathlib.RingTheory.Flat.EquationalCriterion Mathlib.LinearAlgebra.Eigenspace.Semisimple Mathlib.Analysis.Calculus.Conformal.InnerProduct Mathlib.Analysis.Calculus.VectorField Mathlib.FieldTheory.KummerExtension Mathlib.Algebra.Algebra.Subalgebra.IsSimpleOrder Mathlib.LinearAlgebra.QuadraticForm.Isometry Mathlib.RingTheory.Jacobson.Polynomial Mathlib.Topology.Instances.Irrational Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition Mathlib.Analysis.Complex.Arg Mathlib.Geometry.Manifold.Algebra.Monoid Mathlib.FieldTheory.Minpoly.Field Mathlib.LinearAlgebra.UnitaryGroup Mathlib.Topology.Algebra.Module.Determinant Mathlib.SetTheory.Cardinal.Free Mathlib.Algebra.Module.LinearMap.Polynomial Mathlib.Analysis.MellinInversion Mathlib.RepresentationTheory.GroupCohomology.LowDegree Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear Mathlib.LinearAlgebra.BilinearForm.TensorProduct Mathlib.Analysis.Convex.Cone.InnerDual Mathlib.Geometry.Manifold.Algebra.Structures Mathlib.Algebra.FreeAlgebra.Cardinality Mathlib.Analysis.CStarAlgebra.Hom Mathlib.Analysis.Complex.Polynomial.UnitTrinomial Mathlib.Geometry.Manifold.PartitionOfUnity Mathlib.LinearAlgebra.Dimension.Free Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian Mathlib.Algebra.Lie.BaseChange Mathlib.LinearAlgebra.Dual Mathlib.Analysis.Complex.UpperHalfPlane.Basic Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv Mathlib.Algebra.Lie.CartanMatrix Mathlib.Geometry.Manifold.MFDeriv.Atlas Mathlib.MeasureTheory.Measure.SeparableMeasure Mathlib.MeasureTheory.Covering.Differentiation Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange Mathlib.NumberTheory.LSeries.HurwitzZetaOdd Mathlib.RingTheory.FractionalIdeal.Operations Mathlib.LinearAlgebra.QuadraticForm.TensorProduct Mathlib.ModelTheory.Algebra.Field.IsAlgClosed Mathlib.Analysis.Complex.Hadamard Mathlib.RingTheory.Etale.Basic Mathlib.RingTheory.LinearDisjoint Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap Mathlib.Geometry.Manifold.Algebra.LieGroup Mathlib.Algebra.Lie.UniversalEnveloping Mathlib.FieldTheory.JacobsonNoether Mathlib.LinearAlgebra.Dimension.Torsion.Basic Mathlib.Combinatorics.SimpleGraph.LapMatrix Mathlib.Analysis.BoundedVariation Mathlib.Analysis.InnerProductSpace.Adjoint Mathlib.Analysis.InnerProductSpace.Semisimple 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.Algebra.Lie.Subalgebra Mathlib.Analysis.Convex.Cone.Proper Mathlib.Probability.Distributions.Pareto Mathlib.NumberTheory.DirichletCharacter.Bounds Mathlib.Algebra.Lie.Sl2 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.CategoryTheory.Preadditive.HomOrthogonal Mathlib.Analysis.Calculus.Rademacher Mathlib.Analysis.Convex.Visible Mathlib.Analysis.Calculus.BumpFunction.InnerProduct Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace Mathlib.LinearAlgebra.Matrix.Spectrum Mathlib.RingTheory.WittVector.IsPoly Mathlib.RingTheory.Kaehler.TensorProduct Mathlib.LinearAlgebra.Dimension.Constructions Mathlib.MeasureTheory.Integral.Pi Mathlib.LinearAlgebra.Dimension.ErdosKaplansky Mathlib.Analysis.Normed.Module.Complemented Mathlib.Analysis.InnerProductSpace.l2Space Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap Mathlib.Algebra.Lie.Solvable Mathlib.Analysis.Complex.UpperHalfPlane.Exp Mathlib.NumberTheory.NumberField.Embeddings Mathlib.MeasureTheory.Function.Intersectivity Mathlib.Algebra.Lie.Weights.Cartan Mathlib.Probability.Process.Filtration Mathlib.MeasureTheory.Integral.Periodic Mathlib.RingTheory.Valuation.Minpoly Mathlib.Algebra.QuaternionBasis Mathlib.NumberTheory.Harmonic.Bounds Mathlib.RingTheory.Artinian.Instances Mathlib.LinearAlgebra.SymplecticGroup Mathlib.Geometry.Manifold.AnalyticManifold Mathlib.Analysis.MellinTransform Mathlib.LinearAlgebra.Determinant Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating Mathlib.Analysis.Convex.StrictConvexBetween 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.LinearAlgebra.Dimension.StrongRankCondition Mathlib.Analysis.Convex.SpecificFunctions.Deriv Mathlib.Analysis.Normed.Module.WeakDual Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd Mathlib.MeasureTheory.Integral.SetToL1 Mathlib.Algebra.Lie.Engel Mathlib.Analysis.Calculus.FDeriv.Symmetric Mathlib.RingTheory.WittVector.Defs Mathlib.Algebra.Category.ModuleCat.Free Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear Mathlib.RingTheory.FiniteLength Mathlib.Geometry.Euclidean.Inversion.Basic Mathlib.Algebra.Lie.Rank Mathlib.Probability.Kernel.Condexp Mathlib.RingTheory.IntegralClosure.Algebra.Basic Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator Mathlib.LinearAlgebra.AffineSpace.Matrix Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv Mathlib.FieldTheory.PerfectClosure Mathlib.LinearAlgebra.CliffordAlgebra.Prod Mathlib.LinearAlgebra.Eigenspace.Pi Mathlib.FieldTheory.Galois.Infinite Mathlib.Algebra.Lie.Classical Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries Mathlib.Algebra.Polynomial.Bivariate Mathlib.Geometry.Euclidean.Triangle 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.RingTheory.FiniteType Mathlib.Geometry.Manifold.DerivationBundle Mathlib.LinearAlgebra.Eigenspace.Minpoly Mathlib.Probability.Density Mathlib.LinearAlgebra.Projectivization.Subspace Mathlib.Analysis.Complex.OpenMapping Mathlib.Probability.ProbabilityMassFunction.Integrals Mathlib.Data.Complex.Orientation Mathlib.RingTheory.Polynomial.RationalRoot Mathlib.RingTheory.WittVector.FrobeniusFractionField Mathlib.LinearAlgebra.Matrix.ToLinearEquiv Mathlib.Analysis.Calculus.BumpFunction.Normed Mathlib.Analysis.NormedSpace.Connected Mathlib.Geometry.Manifold.IntegralCurve.Transform Mathlib.Analysis.ODE.PicardLindelof Mathlib.RingTheory.RootsOfUnity.Minpoly Mathlib.Probability.ConditionalExpectation Mathlib.FieldTheory.Tower Mathlib.MeasureTheory.Integral.SetIntegral Mathlib.Analysis.Analytic.Polynomial Mathlib.Analysis.InnerProductSpace.ConformalLinearMap Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv Mathlib.RingTheory.WittVector.DiscreteValuationRing Mathlib.Geometry.Manifold.LocalDiffeomorph Mathlib.FieldTheory.PolynomialGaloisGroup Mathlib.Analysis.InnerProductSpace.Orientation Mathlib.Geometry.Euclidean.Angle.Oriented.Affine Mathlib.NumberTheory.ModularForms.CongruenceSubgroups Mathlib.LinearAlgebra.Dimension.Finite Mathlib.LinearAlgebra.RootSystem.RootPositive Mathlib.NumberTheory.LSeries.HurwitzZeta Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform Mathlib.MeasureTheory.Function.LpSpace.DomAct.Continuous Mathlib.Geometry.Euclidean.PerpBisector Mathlib.MeasureTheory.Group.Integral Mathlib.LinearAlgebra.Matrix.IsDiag Mathlib.Analysis.Convex.Radon Mathlib.Algebra.Lie.TensorProduct 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.RepresentationTheory.Maschke Mathlib.RingTheory.Kaehler.JacobiZariski Mathlib.Probability.Integration Mathlib.Analysis.Distribution.SchwartzSpace Mathlib.NumberTheory.Bertrand Mathlib.RingTheory.NormTrace Mathlib.RingTheory.Derivation.MapCoeffs Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber Mathlib.LinearAlgebra.RootSystem.Hom Mathlib.Analysis.SpecialFunctions.Gamma.Deriv Mathlib.Geometry.Manifold.Metrizable Mathlib.Analysis.BoxIntegral.DivergenceTheorem Mathlib.NumberTheory.LSeries.Convolution Mathlib.LinearAlgebra.Dimension.RankNullity Mathlib.LinearAlgebra.Basis.Flag Mathlib.LinearAlgebra.Matrix.NonsingularInverse Mathlib.Algebra.Lie.InvariantForm Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic Mathlib.Analysis.SpecialFunctions.Pow.Integral Mathlib.Geometry.Manifold.WhitneyEmbedding Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis Mathlib.Algebra.Lie.CartanExists Mathlib.RingTheory.Localization.Away.AdjoinRoot Mathlib.Probability.Kernel.Integral Mathlib.MeasureTheory.Integral.Average 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.Algebra.DirectSum.LinearMap Mathlib.Probability.CDF Mathlib.LinearAlgebra.ExteriorAlgebra.Basic Mathlib.NumberTheory.EulerProduct.ExpLog Mathlib.NumberTheory.FLT.Polynomial Mathlib.RingTheory.AlgebraicIndependent.Adjoin Mathlib.LinearAlgebra.Matrix.Dual Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique Mathlib.RingTheory.LocalProperties.Projective Mathlib.MeasureTheory.Measure.Haar.OfBasis Mathlib.Data.Complex.ExponentialBounds Mathlib.Analysis.InnerProductSpace.TwoDim Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic Mathlib.Probability.Martingale.Centering Mathlib.Algebra.Lie.OfAssociative Mathlib.LinearAlgebra.QuadraticForm.Dual Mathlib.NumberTheory.ModularForms.QExpansion Mathlib.MeasureTheory.Measure.Haar.Quotient Mathlib.Topology.Instances.RatLemmas Mathlib.Geometry.Manifold.Instances.Sphere Mathlib.NumberTheory.DiophantineApproximation.Basic Mathlib.LinearAlgebra.Matrix.Block Mathlib.Geometry.Manifold.VectorBundle.SmoothSection Mathlib.Geometry.Manifold.ContMDiff.Product Mathlib.LinearAlgebra.RootSystem.Defs Mathlib.Analysis.InnerProductSpace.LaxMilgram Mathlib.LinearAlgebra.Projectivization.Basic Mathlib.RingTheory.WittVector.MulP Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate Mathlib.Data.Nat.Factorial.SuperFactorial |
1 |
Declarations diff
+ DivisionSemiring.instIsArtinianRing
+ RingEquiv.isArtinianRing
+ instance {R S} [Semiring R] [Semiring S] [IsArtinianRing R] [IsArtinianRing S] :
+ instance {R S} [Semiring R] [Semiring S] [IsNoetherianRing R] [IsNoetherianRing S] :
+ instance {ι} [Finite ι] (R : ι → Type*) [Π i, Ring (R i)] [∀ i, IsSemisimpleRing (R i)] :
+ instance {ι} [Finite ι] : ∀ {R : ι → Type*} [Π i, Semiring (R i)] [∀ i, IsArtinianRing (R i)],
+ instance {ι} [Finite ι] : ∀ {R : ι → Type*} [Π i, Semiring (R i)] [∀ i, IsNoetherianRing (R i)],
+ isArtinianRing_rangeS
+ isNoetherianRing_rangeS
- instance {ι} [Finite ι] (R : ι → Type*) [∀ i, Ring (R i)] [∀ i, IsSemisimpleRing (R i)] :
-++ piOptionEquivProd
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
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
d6896c6 to
9889092
Compare
Contributor
|
Pull request successfully merged into master. Build succeeded: |
Julian
added a commit
that referenced
this pull request
Jan 8, 2025
* 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
* 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) ...
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.