integralClosure — Mathlib

English

In a ring of dimension ≤ 1, there do not exist a chain p0 < p1 < p2 of prime ideals.

Русский

В кольце размерности ≤ 1 не существует цепочки простых идеалов p0 < p1 < p2.

LaTeX

$$¬(p0 < p1 ∧ p1 < p2)$$

Lean4

nonrec instance integralClosure [Nontrivial R] [IsDomain A] [Algebra R A] [DimensionLEOne R] :
    DimensionLEOne (integralClosure R A) :=
  DimensionLEOne.isIntegralClosure R A (integralClosure R A)

Похожие утверждения