ringKrullDim_eq_zero_of_isField — Mathlib

English

If F is a field (commutative ring with every nonzero element invertible), then its Krull dimension is zero.

Русский

Если F — поле, то его размерность Крull равна нулю.

LaTeX

$$$\text{IsField}(F) \Rightarrow \operatorname{ringKrullDim}(F) = 0$$$

Lean4

theorem ringKrullDim_eq_zero_of_isField {F : Type*} [CommRing F] (hF : IsField F) : ringKrullDim F = 0 :=
  @krullDim_eq_zero_of_unique _ _ <| @PrimeSpectrum.instUnique _ hF.toField

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