Commit 2025-01-07 20:33 ed32f2fc

View on Github →

chore(Noetherian/Artinian): generalize to Semiring (#20534)

Estimated changes

Modified Mathlib/Algebra/Ring/Equiv.lean

added def RingEquiv.piOptionEquivProd

Modified Mathlib/LinearAlgebra/LinearIndependent.lean

Modified Mathlib/LinearAlgebra/Pi.lean

modified def LinearEquiv.piOptionEquivProd

modified theorem LinearMap.lsum_single

Modified Mathlib/RingTheory/Artinian/Module.lean

modified theorem Function.Surjective.isArtinianRing

modified theorem IsArtinianRing.subtype_isMaximal_finite

modified theorem Ring.isArtinian_of_zero_eq_one

added theorem RingEquiv.isArtinianRing

modified theorem isArtinianRing_iff

modified theorem isArtinian_of_submodule_of_artinian

modified theorem isArtinian_of_tower

Modified Mathlib/RingTheory/Artinian/Ring.lean

Modified Mathlib/RingTheory/Ideal/Maps.lean

modified theorem Ideal.NoZeroSMulDivisors.ker_algebraMap_eq_bot

modified theorem Ideal.RingHom.ker_isMaximal_of_surjective

modified theorem Ideal.RingHom.ker_isPrime

modified def Ideal.orderEmbeddingOfSurjective

Modified Mathlib/RingTheory/Ideal/Prod.lean

modified def Ideal.idealProdEquiv

modified def Ideal.prod

Modified Mathlib/RingTheory/Noetherian/Basic.lean

modified theorem isNoetherianRing_of_ringEquiv

modified theorem isNoetherianRing_of_surjective

modified theorem isNoetherian_of_range_eq_ker

Modified Mathlib/RingTheory/Noetherian/Nilpotent.lean

modified theorem IsNoetherianRing.isNilpotent_nilradical

Modified Mathlib/RingTheory/SimpleModule.lean