ringKrullDim_eq_one — Mathlib

English

If R is a domain and a principal ideal ring but not a field, then the Krull dimension equals 1: ringKrullDim R = 1.

Русский

Если R является доменом и кольцом, образованным одним идеалом, но не является полем, то размерность Крулля равна 1: ringKrullDim R = 1.

LaTeX

$$$\\operatorname{ringKrullDim} R = 1$$$

Lean4

theorem ringKrullDim_eq_one (R : Type*) [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] (h : ¬IsField R) :
    ringKrullDim R = 1 := by
  apply eq_of_le_of_not_lt ?_ fun h' ↦ h ?_
  · rw [← Nat.cast_one, ← Ring.krullDimLE_iff]
    infer_instance
  · have h'' : ringKrullDim R ≤ 0 := Order.le_of_lt_succ h'
    rw [← Nat.cast_zero, ← Ring.krullDimLE_iff] at h''
    exact Ring.KrullDimLE.isField_of_isDomain

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