Theorems · Theorem · commutative algebra
IsLocalRing.mem_maximalIdeal
∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : IsLocalRing R] (x : R),
x ∈ IsLocalRing.maximalIdeal R ↔ x ∈ nonunits R- Cited by
- 6 results in Mathlib
- Foundations
- Depth 27 from the axioms · uses propext
- Assumes
- CommSemiringIsLocalRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- CommSemiringstatement and proof · cited by 10,911
- Idealstatement · cited by 4,748
- IsLocalRingstatement and proof · cited by 339
- IsLocalRing.maximalIdealstatement · cited by 297
- nonunitsstatement · cited by 35
Cited by6
Results whose statement or proof uses this declaration.
- ValuationSubring.valuation_lt_one_iffproof · cited by 4
- PadicInt.norm_sub_zmodRepr_lt_oneproof · cited by 2
- ArchimedeanClass.FiniteResidueField.mk_eq_mkproof · cited by 1
- charP_zero_or_prime_powerproof · cited by 1
- IsDiscreteValuationRing.RingEquivClass.isDiscreteValuationRingproof · cited by 0
- HenselianLocalRing.TFAEproof · cited by 0