feat(RingTheory): Artinian rings over Jacobson rings

[alreadydone]

Co-authored-by: Andrew Yang

---

[github-actions]

PR summary a8bd6594bb

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Module.Submodule.Range	643	645	+2 (+0.31%)
Mathlib.RingTheory.Finiteness.Finsupp	972	975	+3 (+0.31%)

Import changes for all files

Files	Import difference
40 files Mathlib.Algebra.Lie.Basic Mathlib.Algebra.Module.Submodule.Equiv Mathlib.Algebra.Module.Submodule.Range Mathlib.Algebra.MonoidAlgebra.Degree Mathlib.Algebra.MonoidAlgebra.Support Mathlib.Algebra.Polynomial.BigOperators Mathlib.Algebra.Polynomial.CancelLeads Mathlib.Algebra.Polynomial.Coeff Mathlib.Algebra.Polynomial.Degree.Definitions Mathlib.Algebra.Polynomial.Degree.Domain Mathlib.Algebra.Polynomial.Degree.Lemmas Mathlib.Algebra.Polynomial.Degree.Monomial Mathlib.Algebra.Polynomial.Degree.Operations Mathlib.Algebra.Polynomial.Degree.SmallDegree Mathlib.Algebra.Polynomial.Degree.Support Mathlib.Algebra.Polynomial.Degree.TrailingDegree Mathlib.Algebra.Polynomial.Degree.Units Mathlib.Algebra.Polynomial.Derivative Mathlib.Algebra.Polynomial.Div Mathlib.Algebra.Polynomial.EraseLead Mathlib.Algebra.Polynomial.Eval.Coeff Mathlib.Algebra.Polynomial.Eval.Degree Mathlib.Algebra.Polynomial.Eval.Irreducible Mathlib.Algebra.Polynomial.Eval.SMul Mathlib.Algebra.Polynomial.Eval.Subring Mathlib.Algebra.Polynomial.Identities Mathlib.Algebra.Polynomial.Inductions Mathlib.Algebra.Polynomial.Mirror Mathlib.Algebra.Polynomial.Monic Mathlib.Algebra.Polynomial.Reverse Mathlib.Algebra.Polynomial.UnitTrinomial Mathlib.Data.Finsupp.Weight Mathlib.Data.Nat.Choose.Vandermonde Mathlib.LinearAlgebra.BilinearMap Mathlib.LinearAlgebra.Countable Mathlib.LinearAlgebra.Finsupp.LinearCombination Mathlib.LinearAlgebra.Finsupp.Supported Mathlib.RingTheory.Polynomial.Hermite.Basic Mathlib.RingTheory.Polynomial.Opposites Mathlib.Tactic.ComputeDegree	2
Mathlib.RingTheory.Finiteness.Finsupp Mathlib.RingTheory.Finiteness.Ideal	3
Mathlib.RingTheory.Jacobson.Artinian (new file)	1608

---

Declarations diff

+ Module.finite_iff_isArtinianRing
+ Module.finite_iff_krullDimLE_zero
+ Module.finite_of_isArtinianRing
+ Module.finite_of_isSemisimpleRing
+ _root_.LinearMap.finite_iff_of_bijective
+ _root_.Module.Finite.of_submodule_quotient
+ finite_of_isArtinian
+ finite_of_isNoetherian
+ induction
+ instance (priority := 900) (R) [CommRing R] [IsSemisimpleRing R] : IsReduced R
+ isNoetherian_iff_isArtinian
+ jacobson_eq_sInf_isMaximal
+ nilradical_eq_bot_iff
+ nilradical_le_jacobson
+ range_restrictScalars
+ restrictScalars_map
- IsSemiprimaryRing.isNoetherian_iff_isArtinian

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

[riccardobrasca]

Suggested change

	instance (priority := 900) (R) [CommRing R] [IsSemisimpleRing R] : IsReduced R where
	instance (priority := low) (R) [CommRing R] [IsSemisimpleRing R] : IsReduced R where

Seems the standard way, unless you have a specific reason for 900.

[alreadydone]

I'm following Andrew's advice, though I'm not exactly sure whether it applies here.

[riccardobrasca]

Same.

[alreadydone]

finite_of_finite_type_of_isJacobsonRing isn't an instance yet, so I didn't make these instances. Module.Finite.finiteType is a priority 100 instance, so these should probably get an even lower priority if made instances due to the loopiness. Similar lemmas like Module.finitePresentation_of_finite are not made instances due to performance reasons.

Also note that this lemma implies the previous one because Lean can infer that an semisimple ring is artinian.

[riccardobrasca]

Can you try so we can see the regression? If it is really bad no problem in keeping them as theorem (adding a comment).

[alreadydone]

!bench

[leanprover-bot]

Here are the benchmark results for commit a8bd659.
The entire run failed.
Found no significant differences.