[Merged by Bors] - feat(RingTheory): Hopkins–Levitzki theorem by alreadydone · Pull Request #21451 · leanprover-community/mathlib4

alreadydone · 2025-02-05T04:56:22Z

RingTheory/HopkinsLevitzki.lean (new file): the Hopkins--Levitzki theorem says a module over a semiprimary ring is Noetherian iff it's Artinian (iff it's of finite length). As a consequence, a (left) Artinian ring is also (left) Noetherian, and a commutative ring is Artinian iff it's Noetherian and has Krull dimension 0.

RingTheory/Jacobson/Semiprimary.lean (new file): contains the definition of semiprimary rings, and connections between Jacobson radicals of modules and semisimplicity.

RingTheory/Jacobson/Radical.lean (new file): develop the theory of Jacobson radicals of modules, including versions of Nakayama's lemma over noncommutative rings.

RingTheory/Artinian/Module.lean: show an Artinian module or ring is semisimple iff it has trivial radical; show that an Artinian ring is semiprimary.

depends on: [Merged by Bors] - feat: Prerequisites for Hopkins–Levitzki theorem #21544

github-actions · 2025-02-05T04:57:18Z

PR summary dc2957ba01

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.Artinian.Module	1169	1183	+14 (+1.20%)
Mathlib.RingTheory.Artinian.Ring	1190	1202	+12 (+1.01%)
Mathlib.RingTheory.Jacobson.Ideal	1066	1074	+8 (+0.75%)
Mathlib.AlgebraicGeometry.Fiber	2066	2075	+9 (+0.44%)

Import changes for all files

Files	Import difference
248 files `Mathlib.Algebra.Category.ModuleCat.Differentials.Basic` `Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf` `Mathlib.Algebra.Category.Ring.LinearAlgebra` `Mathlib.Algebra.Category.Ring.Under.Limits` `Mathlib.Algebra.GCDMonoid.IntegrallyClosed` `Mathlib.Algebra.Module.DedekindDomain` `Mathlib.Algebra.Module.PID` `Mathlib.Algebra.Module.Presentation.Differentials` `Mathlib.AlgebraicGeometry.AffineScheme` `Mathlib.AlgebraicGeometry.Cover.MorphismProperty` `Mathlib.AlgebraicGeometry.Cover.Open` `Mathlib.AlgebraicGeometry.Cover.Over` `Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic` `Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree` `Mathlib.AlgebraicGeometry.EllipticCurve.Group` `Mathlib.AlgebraicGeometry.FunctionField` `Mathlib.AlgebraicGeometry.GammaSpecAdjunction` `Mathlib.AlgebraicGeometry.GluingOneHypercover` `Mathlib.AlgebraicGeometry.Gluing` `Mathlib.AlgebraicGeometry.IdealSheaf` `Mathlib.AlgebraicGeometry.Limits` `Mathlib.AlgebraicGeometry.Modules.Presheaf` `Mathlib.AlgebraicGeometry.Modules.Sheaf` `Mathlib.AlgebraicGeometry.Modules.Tilde` `Mathlib.AlgebraicGeometry.Morphisms.AffineAnd` `Mathlib.AlgebraicGeometry.Morphisms.Affine` `Mathlib.AlgebraicGeometry.Morphisms.Basic` `Mathlib.AlgebraicGeometry.Morphisms.Constructors` `Mathlib.AlgebraicGeometry.Morphisms.Etale` `Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation` `Mathlib.AlgebraicGeometry.Morphisms.Flat` `Mathlib.AlgebraicGeometry.Morphisms.IsIso` `Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion` `Mathlib.AlgebraicGeometry.Morphisms.Preimmersion` `Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact` `Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated` `Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties` `Mathlib.AlgebraicGeometry.Morphisms.Smooth` `Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks` `Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap` `Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective` `Mathlib.AlgebraicGeometry.OpenImmersion` `Mathlib.AlgebraicGeometry.Over` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme` `Mathlib.AlgebraicGeometry.Properties` `Mathlib.AlgebraicGeometry.PullbackCarrier` `Mathlib.AlgebraicGeometry.Pullbacks` `Mathlib.AlgebraicGeometry.ResidueField` `Mathlib.AlgebraicGeometry.Restrict` `Mathlib.AlgebraicGeometry.Scheme` `Mathlib.AlgebraicGeometry.Sites.BigZariski` `Mathlib.AlgebraicGeometry.Sites.Etale` `Mathlib.AlgebraicGeometry.Sites.MorphismProperty` `Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski` `Mathlib.AlgebraicGeometry.Sites.Small` `Mathlib.AlgebraicGeometry.Spec` `Mathlib.AlgebraicGeometry.Stalk` `Mathlib.AlgebraicGeometry.StructureSheaf` `Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality` `Mathlib.Analysis.Fourier.ZMod` `Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar` `Mathlib.FieldTheory.Finite.Trace` `Mathlib.FieldTheory.Laurent` `Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed` `Mathlib.FieldTheory.Minpoly.MinpolyDiv` `Mathlib.FieldTheory.RatFunc.AsPolynomial` `Mathlib.FieldTheory.RatFunc.Degree` `Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace` `Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField` `Mathlib.GroupTheory.FiniteAbelian.Basic` `Mathlib.GroupTheory.FiniteAbelian.Duality` `Mathlib.NumberTheory.BernoulliPolynomials` `Mathlib.NumberTheory.Bernoulli` `Mathlib.NumberTheory.ClassNumber.Finite` `Mathlib.NumberTheory.ClassNumber.FunctionField` `Mathlib.NumberTheory.Cyclotomic.Basic` `Mathlib.NumberTheory.Cyclotomic.Discriminant` `Mathlib.NumberTheory.Cyclotomic.Embeddings` `Mathlib.NumberTheory.Cyclotomic.Gal` `Mathlib.NumberTheory.Cyclotomic.PID` `Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots` `Mathlib.NumberTheory.Cyclotomic.Rat` `Mathlib.NumberTheory.Cyclotomic.Three` `Mathlib.NumberTheory.DirichletCharacter.GaussSum` `Mathlib.NumberTheory.DirichletCharacter.Orthogonality` `Mathlib.NumberTheory.FLT.Three` `Mathlib.NumberTheory.Fermat` `Mathlib.NumberTheory.FunctionField` `Mathlib.NumberTheory.GaussSum` `Mathlib.NumberTheory.JacobiSum.Basic` `Mathlib.NumberTheory.KummerDedekind` `Mathlib.NumberTheory.LSeries.DirichletContinuation` `Mathlib.NumberTheory.LSeries.HurwitzZetaValues` `Mathlib.NumberTheory.LSeries.Nonvanishing` `Mathlib.NumberTheory.LSeries.PrimesInAP` `Mathlib.NumberTheory.LSeries.ZMod` `Mathlib.NumberTheory.LegendreSymbol.AddCharacter` `Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol` `Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum` `Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity` `Mathlib.NumberTheory.MulChar.Duality` `Mathlib.NumberTheory.NumberField.AdeleRing` `Mathlib.NumberTheory.NumberField.Basic` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone` `Mathlib.NumberTheory.NumberField.ClassNumber` `Mathlib.NumberTheory.NumberField.Completion` `Mathlib.NumberTheory.NumberField.Discriminant.Basic` `Mathlib.NumberTheory.NumberField.Discriminant.Defs` `Mathlib.NumberTheory.NumberField.Embeddings` `Mathlib.NumberTheory.NumberField.EquivReindex` `Mathlib.NumberTheory.NumberField.FinitePlaces` `Mathlib.NumberTheory.NumberField.FractionalIdeal` `Mathlib.NumberTheory.NumberField.House` `Mathlib.NumberTheory.NumberField.Norm` `Mathlib.NumberTheory.NumberField.ProductFormula` `Mathlib.NumberTheory.NumberField.Units.Basic` `Mathlib.NumberTheory.NumberField.Units.DirichletTheorem` `Mathlib.NumberTheory.NumberField.Units.Regulator` `Mathlib.NumberTheory.Padics.Hensel` `Mathlib.NumberTheory.Padics.MahlerBasis` `Mathlib.NumberTheory.Padics.PadicIntegers` `Mathlib.NumberTheory.Padics.ProperSpace` `Mathlib.NumberTheory.Padics.RingHoms` `Mathlib.NumberTheory.PrimesCongruentOne` `Mathlib.NumberTheory.RamificationInertia.Basic` `Mathlib.NumberTheory.ZetaValues` `Mathlib.RingTheory.AdicCompletion.Algebra` `Mathlib.RingTheory.AdicCompletion.AsTensorProduct` `Mathlib.RingTheory.AdicCompletion.Exactness` `Mathlib.RingTheory.AdicCompletion.Functoriality` `Mathlib.RingTheory.AdicCompletion.Noetherian` `Mathlib.RingTheory.ClassGroup` `Mathlib.RingTheory.DedekindDomain.AdicValuation` `Mathlib.RingTheory.DedekindDomain.Basic` `Mathlib.RingTheory.DedekindDomain.Different` `Mathlib.RingTheory.DedekindDomain.Dvr` `Mathlib.RingTheory.DedekindDomain.Factorization` `Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing` `Mathlib.RingTheory.DedekindDomain.Ideal` `Mathlib.RingTheory.DedekindDomain.IntegralClosure` `Mathlib.RingTheory.DedekindDomain.PID` `Mathlib.RingTheory.DedekindDomain.SInteger` `Mathlib.RingTheory.DedekindDomain.SelmerGroup` `Mathlib.RingTheory.DiscreteValuationRing.Basic` `Mathlib.RingTheory.DiscreteValuationRing.TFAE` `Mathlib.RingTheory.Discriminant` `Mathlib.RingTheory.DualNumber` `Mathlib.RingTheory.Etale.Basic` `Mathlib.RingTheory.Etale.Kaehler` `Mathlib.RingTheory.Etale.Pi` `Mathlib.RingTheory.Extension` `Mathlib.RingTheory.Filtration` `Mathlib.RingTheory.Flat.Localization` `Mathlib.RingTheory.FractionalIdeal.Norm` `Mathlib.RingTheory.Generators` `Mathlib.RingTheory.Henselian` `Mathlib.RingTheory.Ideal.Cotangent` `Mathlib.RingTheory.Ideal.GoingUp` `Mathlib.RingTheory.Ideal.Norm.AbsNorm` `Mathlib.RingTheory.Ideal.Norm.RelNorm` `Mathlib.RingTheory.IntegralClosure.IntegralRestrict` `Mathlib.RingTheory.IntegralClosure.IntegrallyClosed` `Mathlib.RingTheory.Invariant` `Mathlib.RingTheory.IsAdjoinRoot` `Mathlib.RingTheory.Jacobson.Polynomial` `Mathlib.RingTheory.Kaehler.Basic` `Mathlib.RingTheory.Kaehler.CotangentComplex` `Mathlib.RingTheory.Kaehler.JacobiZariski` `Mathlib.RingTheory.Kaehler.Polynomial` `Mathlib.RingTheory.Kaehler.TensorProduct` `Mathlib.RingTheory.KrullDimension.Basic` `Mathlib.RingTheory.KrullDimension.Field` `Mathlib.RingTheory.LaurentSeries` `Mathlib.RingTheory.LittleWedderburn` `Mathlib.RingTheory.LocalProperties.Basic` `Mathlib.RingTheory.LocalProperties.IntegrallyClosed` `Mathlib.RingTheory.LocalProperties.Projective` `Mathlib.RingTheory.LocalProperties.Reduced` `Mathlib.RingTheory.LocalRing.Module` `Mathlib.RingTheory.LocalRing.Quotient` `Mathlib.RingTheory.LocalRing.ResidueField.Basic` `Mathlib.RingTheory.LocalRing.ResidueField.Ideal` `Mathlib.RingTheory.Localization.Finiteness` `Mathlib.RingTheory.Localization.Free` `Mathlib.RingTheory.Localization.NormTrace` `Mathlib.RingTheory.Nakayama` `Mathlib.RingTheory.Polynomial.Cyclotomic.Basic` `Mathlib.RingTheory.Polynomial.Cyclotomic.Eval` `Mathlib.RingTheory.Polynomial.Cyclotomic.Expand` `Mathlib.RingTheory.Polynomial.Cyclotomic.Roots` `Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral` `Mathlib.RingTheory.Polynomial.GaussLemma` `Mathlib.RingTheory.Polynomial.RationalRoot` `Mathlib.RingTheory.Polynomial.Selmer` `Mathlib.RingTheory.PowerSeries.Derivative` `Mathlib.RingTheory.PowerSeries.Inverse` `Mathlib.RingTheory.Presentation` `Mathlib.RingTheory.RingHom.FinitePresentation` `Mathlib.RingTheory.RingHom.FiniteType` `Mathlib.RingTheory.RingHom.Finite` `Mathlib.RingTheory.RingHom.Flat` `Mathlib.RingTheory.RingHom.Integral` `Mathlib.RingTheory.RingHom.Locally` `Mathlib.RingTheory.RingHom.StandardSmooth` `Mathlib.RingTheory.RingHom.Surjective` `Mathlib.RingTheory.RingHom.Unramified` `Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed` `Mathlib.RingTheory.RootsOfUnity.Minpoly` `Mathlib.RingTheory.Smooth.Basic` `Mathlib.RingTheory.Smooth.Kaehler` `Mathlib.RingTheory.Smooth.Local` `Mathlib.RingTheory.Smooth.Locus` `Mathlib.RingTheory.Smooth.Pi` `Mathlib.RingTheory.Smooth.StandardSmoothCotangent` `Mathlib.RingTheory.Smooth.StandardSmooth` `Mathlib.RingTheory.Spectrum.Maximal.Localization` `Mathlib.RingTheory.Spectrum.Maximal.Topology` `Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet` `Mathlib.RingTheory.Spectrum.Prime.FreeLocus` `Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC` `Mathlib.RingTheory.Spectrum.Prime.Module` `Mathlib.RingTheory.Spectrum.Prime.TensorProduct` `Mathlib.RingTheory.Spectrum.Prime.Topology` `Mathlib.RingTheory.Trace.Basic` `Mathlib.RingTheory.Trace.Quotient` `Mathlib.RingTheory.Unramified.Basic` `Mathlib.RingTheory.Unramified.Finite` `Mathlib.RingTheory.Unramified.Locus` `Mathlib.RingTheory.Unramified.Pi` `Mathlib.RingTheory.Valuation.AlgebraInstances` `Mathlib.RingTheory.Valuation.Integral` `Mathlib.RingTheory.Valuation.LocalSubring` `Mathlib.RingTheory.Valuation.RamificationGroup` `Mathlib.RingTheory.Valuation.ValuationSubring` `Mathlib.RingTheory.WittVector.Compare` `Mathlib.RingTheory.WittVector.Complete` `Mathlib.RingTheory.WittVector.DiscreteValuationRing` `Mathlib.RingTheory.WittVector.FrobeniusFractionField` `Mathlib.RingTheory.WittVector.Isocrystal` `Mathlib.Tactic.NormNum.LegendreSymbol` `Mathlib.Tactic` `Mathlib.Topology.Algebra.Valued.LocallyCompact` `Mathlib.Topology.Algebra.Valued.NormedValued` `Mathlib.Topology.Algebra.Valued.ValuationTopology` `Mathlib.Topology.Algebra.Valued.ValuedField`	1
16 files `Mathlib.Algebra.Lie.Weights.Killing` `Mathlib.Algebra.Lie.Weights.RootSystem` `Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified` `Mathlib.Analysis.InnerProductSpace.JointEigenspace` `Mathlib.Analysis.InnerProductSpace.Semisimple` `Mathlib.FieldTheory.JacobsonNoether` `Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation` `Mathlib.LinearAlgebra.Eigenspace.Semisimple` `Mathlib.LinearAlgebra.JordanChevalley` `Mathlib.LinearAlgebra.Semisimple` `Mathlib.RingTheory.Artinian.Instances` `Mathlib.RingTheory.Etale.Field` `Mathlib.RingTheory.FiniteLength` `Mathlib.RingTheory.Regular.RegularSequence` `Mathlib.RingTheory.Unramified.Field` `Mathlib.RingTheory.Unramified.LocalRing`	2
6 files `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf` `Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits` `Mathlib.Geometry.RingedSpace.LocallyRingedSpace` `Mathlib.Geometry.RingedSpace.OpenImmersion` `Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing` `Mathlib.Topology.Sheaves.CommRingCat`	5
`Mathlib.Topology.Algebra.IsOpenUnits`	6
19 files `Mathlib.Algebra.Category.Ring.Constructions` `Mathlib.Algebra.Category.Ring.Instances` `Mathlib.Algebra.Category.Ring.Under.Basic` `Mathlib.Algebra.CharP.LocalRing` `Mathlib.Algebra.CharP.MixedCharZero` `Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization` `Mathlib.RingTheory.Ideal.MinimalPrime.Localization` `Mathlib.RingTheory.LocalProperties.Exactness` `Mathlib.RingTheory.LocalProperties.Submodule` `Mathlib.RingTheory.LocalRing.LocalSubring` `Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic` `Mathlib.RingTheory.LocalRing.ResidueField.Defs` `Mathlib.RingTheory.LocalRing.RingHom.Basic` `Mathlib.RingTheory.Localization.AsSubring` `Mathlib.RingTheory.Localization.AtPrime` `Mathlib.RingTheory.Localization.LocalizationLocalization` `Mathlib.RingTheory.RingHom.Injective` `Mathlib.RingTheory.RingHomProperties` `Mathlib.RingTheory.SurjectiveOnStalks`	7
4 files `Mathlib.LinearAlgebra.Matrix.Ideal` `Mathlib.RingTheory.AdicCompletion.Basic` `Mathlib.RingTheory.Jacobson.Ideal` `Mathlib.RingTheory.SimpleRing.Matrix`	8
18 files `Mathlib.AlgebraicGeometry.AffineSpace` `Mathlib.AlgebraicGeometry.Fiber` `Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion` `Mathlib.AlgebraicGeometry.Morphisms.FiniteType` `Mathlib.AlgebraicGeometry.Morphisms.Finite` `Mathlib.AlgebraicGeometry.Morphisms.Immersion` `Mathlib.AlgebraicGeometry.Morphisms.Integral` `Mathlib.AlgebraicGeometry.Morphisms.Proper` `Mathlib.AlgebraicGeometry.Morphisms.Separated` `Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed` `Mathlib.AlgebraicGeometry.PointsPi` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper` `Mathlib.AlgebraicGeometry.RationalMap` `Mathlib.AlgebraicGeometry.SpreadingOut` `Mathlib.AlgebraicGeometry.ValuativeCriterion` `Mathlib.FieldTheory.AxGrothendieck` `Mathlib.ModelTheory.Algebra.Ring.Definability` `Mathlib.RingTheory.Spectrum.Prime.Polynomial`	9
3 files `Mathlib.AlgebraicGeometry.Noetherian` `Mathlib.RingTheory.Spectrum.Prime.Jacobson` `Mathlib.RingTheory.Spectrum.Prime.Noetherian`	10
20 files `Mathlib.Algebra.Lie.CartanExists` `Mathlib.Algebra.Lie.CartanSubalgebra` `Mathlib.Algebra.Lie.Character` `Mathlib.Algebra.Lie.Derivation.Killing` `Mathlib.Algebra.Lie.EngelSubalgebra` `Mathlib.Algebra.Lie.Engel` `Mathlib.Algebra.Lie.InvariantForm` `Mathlib.Algebra.Lie.Killing` `Mathlib.Algebra.Lie.LieTheorem` `Mathlib.Algebra.Lie.Nilpotent` `Mathlib.Algebra.Lie.Rank` `Mathlib.Algebra.Lie.Semisimple.Lemmas` `Mathlib.Algebra.Lie.Sl2` `Mathlib.Algebra.Lie.TraceForm` `Mathlib.Algebra.Lie.Weights.Basic` `Mathlib.Algebra.Lie.Weights.Cartan` `Mathlib.Algebra.Lie.Weights.Chain` `Mathlib.Algebra.Lie.Weights.Linear` `Mathlib.LinearAlgebra.Eigenspace.Zero` `Mathlib.RingTheory.Nullstellensatz`	11
12 files `Mathlib.Algebra.Lie.CartanMatrix` `Mathlib.Algebra.Lie.Classical` `Mathlib.Algebra.Lie.Matrix` `Mathlib.Algebra.Lie.Normalizer` `Mathlib.Algebra.Lie.Quotient` `Mathlib.Algebra.Lie.Semisimple.Basic` `Mathlib.Algebra.Lie.Semisimple.Defs` `Mathlib.Algebra.Lie.SkewAdjoint` `Mathlib.Algebra.Lie.Solvable` `Mathlib.RingTheory.Artinian.Algebra` `Mathlib.RingTheory.Artinian.Ring` `Mathlib.RingTheory.Jacobson.Ring`	12
15 files `Mathlib.Algebra.Jordan.Basic` `Mathlib.Algebra.Lie.Abelian` `Mathlib.Algebra.Lie.BaseChange` `Mathlib.Algebra.Lie.Derivation.AdjointAction` `Mathlib.Algebra.Lie.Derivation.Basic` `Mathlib.Algebra.Lie.DirectSum` `Mathlib.Algebra.Lie.Extension` `Mathlib.Algebra.Lie.Free` `Mathlib.Algebra.Lie.IdealOperations` `Mathlib.Algebra.Lie.OfAssociative` `Mathlib.Algebra.Lie.Submodule` `Mathlib.Algebra.Lie.TensorProduct` `Mathlib.Algebra.Lie.UniversalEnveloping` `Mathlib.Algebra.Symmetrized` `Mathlib.RingTheory.Derivation.Lie`	13
`Mathlib.Algebra.Lie.Subalgebra` `Mathlib.RingTheory.Artinian.Module`	14
`Mathlib.RingTheory.Jacobson.Radical` (new file)	1050
`Mathlib.RingTheory.Jacobson.Semiprimary` (new file)	1103
`Mathlib.RingTheory.HopkinsLevitzki` (new file)	1597

Declarations diff

+ FG.eq_bot_of_le_jacobson_smul
+ FG.jacobson_smul_lt
+ IsArtinian.isSemisimpleModule_iff_jacobson
+ IsArtinianRing.tfae
+ IsNoetherianRing.isArtinianRing_of_krullDimLE_zero
+ IsSemiprimaryRing
+ IsSemiprimaryRing.isNoetherian_iff_isArtinian
+ IsSemisimpleModule.jacobson_eq_bot
+ IsSemisimpleModule.jacobson_le_annihilator
+ IsSemisimpleModule.jacobson_le_ker
+ IsSemisimpleRing.jacobson_eq_bot
+ IsSimpleModule.jacobson_eq_bot
+ LinearMap.isArtinian_iff_of_bijective
+ Ring.jacobson_eq_nilradical_of_krullDimLE_zero
+ _root_.MaximalSpectrum.toPiLocalizationEquiv
+ coe_jacobson_quotient
+ comap_jacobson_of_bijective
+ comap_jacobson_of_ker_le
+ instance (R) [Ring R] [IsArtinianRing R] (I : Ideal R) [I.IsTwoSided] : IsArtinianRing (R ⧸ I)
+ instance : (jacobson R).IsTwoSided
+ instance : IsSemiprimaryRing R
+ instance [IsArtinianRing R] : IsNoetherianRing R := ((IsArtinianRing.tfae R R).out 2 1).mp ‹_›
+ isArtinianRing_iff_isFiniteLength
+ isArtinianRing_iff_isNoetherianRing_krullDimLE_zero
+ isNoetherian_of_finite_isArtinian
+ isSemisimpleRing_iff_jacobson
+ jacobson_bot
+ jacobson_eq_bot_of_injective
+ jacobson_pi_eq_bot
+ jacobson_pi_le
+ jacobson_smul_lt_top
+ jacobson_smul_top_le
+ map_jacobson_of_bijective
++ jacobson
++ jacobson_le_of_eq_bot
++ jacobson_lt_top
++ jacobson_quotient_jacobson
++ jacobson_quotient_of_le
++ le_comap_jacobson
++ map_jacobson_le
++ map_jacobson_of_ker_le
- MaximalSpectrum.toPiLocalizationEquivtoLocalizationEquiv
- instance (R) [CommRing R] [IsArtinianRing R] (I : Ideal R) : IsArtinianRing (R ⧸ I)

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

Mathlib/RingTheory/HopkinsLevitzki.lean

alreadydone · 2025-02-06T01:40:44Z

!bench

leanprover-bot · 2025-02-06T02:27:51Z

Here are the benchmark results for commit cfe9acc.
There were significant changes against commit fd7df66:

  Benchmark                                 Metric         Change
  ===============================================================
+ ~Mathlib.Algebra.Lie.Weights.Killing      instructions    -5.6%
+ ~Mathlib.Algebra.Lie.Weights.RootSystem   instructions    -6.7%

github-actions · 2025-02-06T02:28:14Z

File	Instructions	%
`build`	+84.764⬝10⁹	(+0.05%)
`lint`	+17.270⬝10⁹	(+0.22%)
`Mathlib.RingTheory.Artinian.Module`	+7.108⬝10⁹	(+18.17%)
`Mathlib.LinearAlgebra.Semisimple`	+4.816⬝10⁹	(+4.33%)
`Mathlib.Algebra.Lie.TraceForm`	+3.239⬝10⁹	(+1.92%)

3 files, Instructions +2.0⬝10⁹

File	Instructions	%
`Mathlib.LinearAlgebra.Span.Basic`	+2.975⬝10⁹	(+6.38%)
`Mathlib.Algebra.Lie.LieTheorem`	+2.360⬝10⁹	(+3.32%)
`Mathlib.AlgebraicGeometry.Noetherian`	+2.264⬝10⁹	(+11.33%)

7 files, Instructions +1.0⬝10⁹

File	Instructions	%
`Mathlib.Algebra.Lie.CartanExists`	+1.704⬝10⁹	(+3.31%)
`Mathlib.RingTheory.Trace.Quotient`	+1.649⬝10⁹	(+2.86%)
`Mathlib.LinearAlgebra.DFinsupp`	+1.530⬝10⁹	(+2.83%)
`Mathlib.Algebra.Lie.Weights.Chain`	+1.289⬝10⁹	(+1.86%)
`Mathlib.AlgebraicGeometry.Morphisms.Separated`	+1.235⬝10⁹	(+3.93%)
`Mathlib.RingTheory.Jacobson.Ring`	+1.148⬝10⁹	(+1.25%)
`Mathlib.Data.Finset.Lattice.Fold`	+1.15⬝10⁹	(+1.87%)

2 files, Instructions -2.0⬝10⁹

File	Instructions	%
`Mathlib.RingTheory.Artinian.Instances`	-1.80⬝10⁹	(-11.17%)
`Mathlib.RingTheory.Noetherian.Basic`	-1.213⬝10⁹	(-4.73%)

File	Instructions	%
`Mathlib.RingTheory.Artinian.Ring`	-5.318⬝10⁹	(-39.57%)
`Mathlib.Algebra.Lie.Weights.RootSystem`	-10.575⬝10⁹	(-6.69%)
`Mathlib.Algebra.Lie.Weights.Killing`	-11.415⬝10⁹	(-5.57%)
CI run

mathlib4-dependent-issues-bot · 2025-02-07T19:32:02Z

This PR/issue depends on:

~~[Merged by Bors] - feat: Prerequisites for Hopkins–Levitzki theorem #21544~~
By Dependent Issues (🤖). Happy coding!

Mathlib/RingTheory/Nullstellensatz.lean

Mathlib/RingTheory/Jacobson/Radical.lean

Mathlib/RingTheory/HopkinsLevitzki.lean

Co-authored-by: Johan Commelin <johan@commelin.net>

jcommelin

Thanks 🎉

bors merge

**RingTheory/HopkinsLevitzki.lean** (new file): the Hopkins--Levitzki theorem says a module over a semiprimary ring is Noetherian iff it's Artinian (iff it's of finite length). As a consequence, a (left) Artinian ring is also (left) Noetherian, and a commutative ring is Artinian iff it's Noetherian and has Krull dimension 0. **RingTheory/Jacobson/Semiprimary.lean** (new file): contains the definition of semiprimary rings, and connections between Jacobson radicals of modules and semisimplicity. **RingTheory/Jacobson/Radical.lean** (new file): develop the theory of Jacobson radicals of modules, including versions of Nakayama's lemma over noncommutative rings. **RingTheory/Artinian/Module.lean**: show an Artinian module or ring is semisimple iff it has trivial radical; show that an Artinian ring is semiprimary.

mathlib-bors · 2025-02-12T07:45:28Z

Pull request successfully merged into master.

Build succeeded:

**RingTheory/HopkinsLevitzki.lean** (new file): the Hopkins--Levitzki theorem says a module over a semiprimary ring is Noetherian iff it's Artinian (iff it's of finite length). As a consequence, a (left) Artinian ring is also (left) Noetherian, and a commutative ring is Artinian iff it's Noetherian and has Krull dimension 0. **RingTheory/Jacobson/Semiprimary.lean** (new file): contains the definition of semiprimary rings, and connections between Jacobson radicals of modules and semisimplicity. **RingTheory/Jacobson/Radical.lean** (new file): develop the theory of Jacobson radicals of modules, including versions of Nakayama's lemma over noncommutative rings. **RingTheory/Artinian/Module.lean**: show an Artinian module or ring is semisimple iff it has trivial radical; show that an Artinian ring is semiprimary.

alreadydone added the t-algebra Algebra (groups, rings, fields, etc) label Feb 5, 2025

alreadydone mentioned this pull request Feb 5, 2025

feat: Hopkins–Levitzki theorem #17908

Closed

3 tasks

github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Feb 5, 2025

alreadydone commented Feb 5, 2025

View reviewed changes

Mathlib/RingTheory/HopkinsLevitzki.lean Outdated Show resolved Hide resolved

alreadydone force-pushed the HopkinsLevitzki branch from eed75fa to 726ab04 Compare February 5, 2025 05:12

github-actions bot removed the large-import Automatically added label for PRs with a significant increase in transitive imports label Feb 5, 2025

alreadydone force-pushed the HopkinsLevitzki branch from 726ab04 to 106dae0 Compare February 5, 2025 05:20

leanprover-community deleted a comment from github-actions bot Feb 5, 2025

alreadydone force-pushed the HopkinsLevitzki branch from 106dae0 to d4bf6ac Compare February 5, 2025 05:58

alreadydone added the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 5, 2025

alreadydone force-pushed the HopkinsLevitzki branch 3 times, most recently from 5668a18 to 337b28f Compare February 5, 2025 11:17

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 5, 2025

alreadydone force-pushed the HopkinsLevitzki branch from 337b28f to 4a9e0d7 Compare February 5, 2025 21:58

github-actions bot added large-import Automatically added label for PRs with a significant increase in transitive imports and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Feb 5, 2025

alreadydone force-pushed the HopkinsLevitzki branch 2 times, most recently from 88f1016 to 43ad40c Compare February 5, 2025 22:49

github-actions bot removed the large-import Automatically added label for PRs with a significant increase in transitive imports label Feb 5, 2025

alreadydone force-pushed the HopkinsLevitzki branch from 43ad40c to cb45773 Compare February 5, 2025 23:22

feat(RingTheory): Hopkins–Levitzki theorem

16a0bbe

alreadydone force-pushed the HopkinsLevitzki branch from cb45773 to 16a0bbe Compare February 6, 2025 01:01

remove @[simp] from vanishingIdeal_zeroLocus_eq_radical

cfe9acc

alreadydone removed the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 6, 2025

stacks tags

0893c64

mergify bot mentioned this pull request Feb 7, 2025

[Merged by Bors] - feat: Prerequisites for Hopkins–Levitzki theorem #21544

Closed

reference

a7929ca

mathlib4-dependent-issues-bot added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) and removed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Feb 7, 2025

alreadydone added 2 commits February 7, 2025 14:51

Merge branch 'master' into HopkinsLevitzki

a3193a8

docstring & golf

9ca9e08

jcommelin reviewed Feb 10, 2025

View reviewed changes

Mathlib/RingTheory/Nullstellensatz.lean Outdated Show resolved Hide resolved

Mathlib/RingTheory/Jacobson/Radical.lean Show resolved Hide resolved

Mathlib/RingTheory/Jacobson/Radical.lean Show resolved Hide resolved

Mathlib/RingTheory/HopkinsLevitzki.lean Outdated Show resolved Hide resolved

jcommelin added the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 10, 2025

alreadydone and others added 2 commits February 10, 2025 15:58

Discard changes to Mathlib/RingTheory/Nullstellensatz.lean

b78da94

simp lemmas

e7636fc

Co-authored-by: Johan Commelin <johan@commelin.net>

alreadydone removed the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 10, 2025

alreadydone added 2 commits February 11, 2025 16:02

clarify stacks 00JB

e2d1b4b

correct the name of MaximalSpectrum.toPiLocalizationEquiv

dc2957b

jcommelin reviewed Feb 12, 2025

View reviewed changes

ghost added the ready-to-merge This PR has been sent to bors. label Feb 12, 2025

mathlib-bors bot changed the title ~~feat(RingTheory): Hopkins–Levitzki theorem~~ [Merged by Bors] - feat(RingTheory): Hopkins–Levitzki theorem Feb 12, 2025

mathlib-bors bot closed this Feb 12, 2025

mathlib-bors bot deleted the HopkinsLevitzki branch February 12, 2025 07:45

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(RingTheory): Hopkins–Levitzki theorem#21451

[Merged by Bors] - feat(RingTheory): Hopkins–Levitzki theorem#21451
alreadydone wants to merge 10 commits intomasterfrom
HopkinsLevitzki

alreadydone commented Feb 5, 2025 •

edited

Loading

Uh oh!

github-actions bot commented Feb 5, 2025 •

edited

Loading

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

alreadydone commented Feb 6, 2025

Uh oh!

leanprover-bot commented Feb 6, 2025

Uh oh!

github-actions bot commented Feb 6, 2025

Uh oh!

mathlib4-dependent-issues-bot commented Feb 7, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

jcommelin left a comment

Uh oh!

mathlib-bors bot commented Feb 12, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

Conversation

alreadydone commented Feb 5, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Feb 5, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary dc2957ba01

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

alreadydone commented Feb 6, 2025

Uh oh!

leanprover-bot commented Feb 6, 2025

Uh oh!

github-actions bot commented Feb 6, 2025

Uh oh!

mathlib4-dependent-issues-bot commented Feb 7, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Feb 12, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

alreadydone commented Feb 5, 2025 •

edited

Loading

github-actions bot commented Feb 5, 2025 •

edited

Loading