finite_iff_krullDimLE_zero — Mathlib

English

If A is finite type and Jacobson ring, then A is finite over R if and only if Krull dimension is zero.

Русский

Если A — алгебра конечного типа и кольцо Якобсона, то A конечно над R тогда и только тогда Krull размерность нулевая.

LaTeX

$$Module.finite_iff_krullDimLE_zero$$

Lean4

/-- If `A` is a finite type algebra over an Artinian ring `R`,
then `A` is finite over `R` if and only if `dim A = 0`. -/
theorem finite_iff_krullDimLE_zero [IsArtinianRing R] : Module.Finite R A ↔ Ring.KrullDimLE 0 A :=
  by
  have : IsNoetherianRing A := Algebra.FiniteType.isNoetherianRing R A
  rw [finite_iff_isArtinianRing, isArtinianRing_iff_isNoetherianRing_krullDimLE_zero, and_iff_right this]

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