Documentation

Mathlib.RingTheory.Jacobson.Artinian

Artinian rings over Jacobson rings #

Main results #

If A is a finite type algebra over R, then A is an Artinian ring and R is Jacobson implies A is finite over R.

If A is a finite type algebra over an Artinian ring R, then A is finite over R if and only if A is an Artinian ring.

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.