Commit 2025-02-25 14:06 de7dc62f

View on Github →

feat(RingTheory): Artinian rings over Jacobson rings (#21904)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Module/Submodule/Range.lean

added theorem LinearMap.range_restrictScalars

added theorem Submodule.restrictScalars_map

Modified Mathlib/RingTheory/Artinian/Module.lean

modified theorem LinearMap.isArtinian_iff_of_bijective

Modified Mathlib/RingTheory/Finiteness/Basic.lean

added theorem LinearMap.finite_iff_of_bijective

modified theorem Module.Finite.of_surjective

modified theorem Submodule.fg_of_fg_map_injective

Modified Mathlib/RingTheory/Finiteness/Finsupp.lean

added theorem Module.Finite.of_submodule_quotient

modified theorem Submodule.fg_ker_comp

modified theorem Submodule.fg_of_fg_map_of_fg_inf_ker

Modified Mathlib/RingTheory/HopkinsLevitzki.lean

added theorem IsSemiprimaryRing.finite_of_isArtinian

added theorem IsSemiprimaryRing.finite_of_isNoetherian

modified theorem IsSemiprimaryRing.isNoetherian_iff_isArtinian

Created Mathlib/RingTheory/Jacobson/Artinian.lean

added theorem Module.finite_iff_isArtinianRing

added theorem Module.finite_iff_krullDimLE_zero

added theorem Module.finite_of_isArtinianRing

added theorem Module.finite_of_isSemisimpleRing

Modified Mathlib/RingTheory/Jacobson/Radical.lean

added theorem Ring.jacobson_eq_sInf_isMaximal

Modified Mathlib/RingTheory/Jacobson/Ring.lean

Modified Mathlib/RingTheory/Jacobson/Semiprimary.lean

Modified Mathlib/RingTheory/KrullDimension/Basic.lean

added theorem nilradical_le_jacobson

Modified Mathlib/RingTheory/Nilpotent/Lemmas.lean

added theorem nilradical_eq_bot_iff

Modified Mathlib/RingTheory/Noetherian/Basic.lean

modified theorem LinearMap.isNoetherian_iff_of_bijective