Theorems · Theorem · commutative algebra
IsLocalRing.maximalIdeal_le_jacobson
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsLocalRing R] (I : Ideal R), IsLocalRing.maximalIdeal R ≤ I.jacobson- Cited by
- 16 results in Mathlib
- Foundations
- Depth 64 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommRingIsLocalRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- Set.ofPredproof · cited by 6,101
- Idealstatement and proof · cited by 4,748
- Ideal.IsMaximalproof · cited by 452
- le_of_eqproof · cited by 366
- IsLocalRingstatement and proof · cited by 339
- IsLocalRing.maximalIdealstatement and proof · cited by 297
- Ideal.jacobsonstatement · cited by 88
- le_sInfproof · cited by 51
- IsLocalRing.eq_maximalIdealproof · cited by 20
Cited by16
Results whose statement or proof uses this declaration.
- IsLocalRing.jacobson_eq_maximalIdealproof · cited by 10
- Ideal.ramificationIdx'_eq_one_of_map_localizationproof · cited by 3
- nontrivial_quotSMulTop_of_mem_maximalIdealproof · cited by 2
- IsSMulRegular.subsingleton_linearMap_iffproof · cited by 2
- IsLocalRing.adjoin_residue_eq_top_iff_adjoin_eq_topproof · cited by 2
- IsLocalRing.maximalIdeal_sq_lt_maximalIdealproof · cited by 1
- Ideal.iInf_pow_smul_eq_bot_of_isLocalRingproof · cited by 1
- Module.supportDim_le_supportDim_quotSMulTop_succproof · cited by 1
- Module.supportDim_quotSMulTop_succ_eq_supportDimproof · cited by 1
- Module.support_quotientproof · cited by 1
- IsLocalRing.isWeaklyRegular_of_perm_of_subset_maximalIdealproof · cited by 1
- ModuleCat.projectiveDimension_quotSMulTop_eq_succ_of_isSMulRegularproof · cited by 1