Theorems · Definition · ring theory
Ring.jacobson
(R : Type u_1) → [inst : Ring R] → Ideal R
The Jacobson radical of a ring R is the Jacobson radical of R as an R-module.
- Defined in
- Mathlib.RingTheory.Jacobson.Radical
- Cited by
- 37 results in Mathlib
- Foundations
- Depth 26 from the axioms · uses propext, Quot.sound
- Assumes
- Ring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Ringstatement and proof · cited by 7,463
- Idealstatement · cited by 4,748
- Module.jacobsonproof · cited by 20
Cited by39
Results whose statement or proof uses this declaration.
- Ideal.jacobson_botstatement · cited by 4
- IsLocalRing.ringJacobson_eq_maximalIdealstatement · cited by 4
- IsSemiprimaryRing.isNoetherian_iff_isArtinianproof · cited by 2
- Ring.jacobson_eq_sInf_isMaximalstatement · cited by 2
- ringKrullDim_le_ringKrullDim_quotient_add_spanFinrankstatement and proof · cited by 2
- ringKrullDim_quotSMulTop_succ_eq_ringKrullDim_of_mem_jacobsonstatement and proof · cited by 2
- IsSemiprimaryRing.inductionstatement and proof · cited by 2
- IsNoetherianRing.isArtinianRing_of_krullDimLE_zeroproof · cited by 2
- nilradical_le_jacobsonstatement · cited by 1
- isSemiprimaryRing_iffstatement and proof · cited by 1
- Ideal.ringJacobson_le_jacobsonstatement · cited by 1
- Submodule.FG.jacobson_smul_ltstatement and proof · cited by 1