Theorems · Definition · commutative algebra
IsArtinianRing
(R : Type u_1) → [Semiring R] → Prop
A ring is Artinian if it is Artinian as a module over itself.
Strictly speaking, this should be called IsLeftArtinianRing but we omit the Left for
convenience in the commutative case. For a right Artinian ring, use IsArtinian Rᵐᵒᵖ R.
For equivalent definitions, see Mathlib/RingTheory/Artinian/Ring.lean.
- Defined in
- Mathlib.RingTheory.Artinian.Defs
- Cited by
- 98 results in Mathlib
- Foundations
- Depth 25 from the axioms, rests on 229 definitions · uses propext, Quot.sound
- Assumes
- Semiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Semiringstatement and proof · cited by 13,802
- IsArtinianproof · cited by 69
Cited by104
Results whose statement or proof uses this declaration.
- IsArtinianRing.equivPistatement and proof · cited by 9
- IsArtinianRing.of_finitestatement and proof · cited by 9
- Module.Finite.of_quasiFinitestatement and proof · cited by 7
- IsArtinianRing.primeSpectrumEquivMaximalSpectrumstatement and proof · cited by 7
- Ideal.ramificationIdx_posproof · cited by 5
- Module.End.isSemisimple_of_squarefree_aeval_eq_zeroproof · cited by 4
- isArtinianRing_iff_krullDimLE_zerostatement · cited by 4
- IsArtinianRing.isNilpotent_jacobson_botstatement and proof · cited by 4
- Module.End.IsSemisimple.of_mem_adjoin_pairproof · cited by 3
- Ring.ord_eq_addValproof · cited by 3
- isArtinianRing_iff_isNoetherianRing_krullDimLE_zerostatement and proof · cited by 3
- IsArtinianRing.isUnit_iff_isRightRegularstatement and proof · cited by 3