Theorems · Theorem · commutative algebra

Ring.krullDimLE_zero_and_isLocalRing_tfae

∀ (R : Type u_1) [inst : CommSemiring R],
  [Ring.KrullDimLE 0 R ∧ IsLocalRing R, ∃! I, I.IsPrime, ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x,
      (nilradical R).IsMaximal].TFAE

Defined in: Mathlib.RingTheory.KrullDimension.Zero
Cited by: 7 results in Mathlib
Foundations: Depth 86 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommSemiring

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites33

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.topproof · cited by 9,680
Set.ofPredproof · cited by 6,101
Idealstatement and proof · cited by 4,748
Bot.botproof · cited by 4,720
IsUnitstatement and proof · cited by 1,602
InfSet.sInfproof · cited by 935
Ideal.IsPrimestatement and proof · cited by 827
one_powproof · cited by 521
Iff.notproof · cited by 489
Ideal.IsMaximalstatement and proof · cited by 452
IsLocalRingstatement and proof · cited by 339

Cited by7

Results whose statement or proof uses this declaration.

Ring.KrullDimLE.eq_maximalIdeal_of_isPrimeproof · cited by 2
Ring.KrullDimLE.isNilpotent_iff_mem_maximalIdealproof · cited by 2
isArtinianRing_iff_isNilpotent_maximalIdealproof · cited by 1
Ring.KrullDimLE.of_isMaximal_nilradicalproof · cited by 0
IsLocalRing.of_isMaximal_nilradicalproof · cited by 0
le_isUnit_iff_zero_notMemproof · cited by 0
Ring.KrullDimLE.existsUnique_isPrimeproof · cited by 0