Theorems · Theorem · commutative algebra
IsLocalRing.le_maximalIdeal
∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : IsLocalRing R] {J : Ideal R}, J ≠ ⊤ → J ≤ IsLocalRing.maximalIdeal R- Cited by
- 20 results in Mathlib
- Foundations
- Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommSemiringIsLocalRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommSemiringstatement and proof · cited by 10,911
- Top.topstatement and proof · cited by 9,680
- Idealstatement and proof · cited by 4,748
- Ideal.IsMaximalproof · cited by 452
- IsLocalRingstatement and proof · cited by 339
- IsLocalRing.maximalIdealstatement · cited by 297
- Ideal.exists_le_maximalproof · cited by 47
- IsLocalRing.eq_maximalIdealproof · cited by 20
Cited by20
Results whose statement or proof uses this declaration.
- IsLocalRing.jacobson_eq_maximalIdealproof · cited by 10
- IsLocalRing.specializes_closedPointproof · cited by 6
- Ideal.height_le_spanRank_toENat_of_mem_minimalPrimesproof · cited by 5
- IsLocalRing.le_maximalIdeal_of_isPrimeproof · cited by 3
- IsLocalRing.exists_maximalIdeal_pow_le_of_isArtinianRing_quotientproof · cited by 2
- IsDiscreteValuationRing.iff_pid_with_one_nonzero_primeproof · cited by 2
- LocalSubring.mem_of_isMax_of_isIntegralproof · cited by 1
- maximalIdeal_isPrincipal_of_isDedekindDomainproof · cited by 1
- Ideal.iInf_pow_smul_eq_bot_of_isLocalRingproof · cited by 1
- Ideal.isPrime_nat_iffproof · cited by 1
- Localization.AtPrime.eq_maximalIdeal_iff_under_eqproof · cited by 1
- IsLocalRing.quotient_artinian_of_mem_minimalPrimes_of_isLocalRingproof · cited by 1