Commit 2025-01-02 13:01 df255e23

View on Github →

chore(RingTheory/Artinian): Split out Artinian/Ring.lean (#20350)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Lie/Derivation/Basic.lean

Modified Mathlib/Algebra/Lie/Nilpotent.lean

Modified Mathlib/Algebra/Lie/Quotient.lean

Modified Mathlib/Algebra/Lie/Subalgebra.lean

Modified Mathlib/Algebra/Lie/Submodule.lean

Modified Mathlib/Algebra/Lie/TensorProduct.lean

Modified Mathlib/Algebra/Lie/Weights/Basic.lean

Modified Mathlib/LinearAlgebra/Eigenspace/Zero.lean

Modified Mathlib/LinearAlgebra/Matrix/ZPow.lean

Modified Mathlib/LinearAlgebra/Semisimple.lean

Created Mathlib/RingTheory/Artinian/Instances.lean

added theorem IsArtinianRing.isSemisimpleRing_of_isReduced

Renamed Mathlib/RingTheory/Artinian.lean to Mathlib/RingTheory/Artinian/Module.lean

added theorem IsArtinianRing.isField_of_isDomain

deleted theorem IsArtinianRing.isNilpotent_jacobson_bot

deleted theorem IsArtinianRing.isSemisimpleRing_of_isReduced

deleted theorem IsArtinianRing.localization_artinian

deleted theorem IsArtinianRing.localization_surjective

Created Mathlib/RingTheory/Artinian/Ring.lean

added theorem IsArtinianRing.isNilpotent_jacobson_bot

added theorem IsArtinianRing.localization_artinian

added theorem IsArtinianRing.localization_surjective

Modified Mathlib/RingTheory/FiniteLength.lean

Modified Mathlib/RingTheory/Jacobson/Ring.lean

Modified Mathlib/RingTheory/Noetherian/Defs.lean

added theorem LinearMap.eventually_disjoint_ker_pow_range_pow

added theorem LinearMap.eventually_iSup_ker_pow_eq

Modified Mathlib/RingTheory/Noetherian/Orzech.lean

deleted theorem LinearMap.eventually_disjoint_ker_pow_range_pow

deleted theorem LinearMap.eventually_iSup_ker_pow_eq

Modified Mathlib/RingTheory/Regular/RegularSequence.lean

Modified Mathlib/RingTheory/Unramified/Field.lean