Documentation

Mathlib.RingTheory.Artinian.Algebra

Algebras over artinian rings #

In this file we collect results about algebras over artinian rings.

In an R-algebra over an artinian ring R, if an element is integral and is not a zero divisor, then it is a unit.

Integral element of an algebra over artinian ring R is either a zero divisor or a unit.

In an R-algebra over an artinian ring R, if an element is integral and is not a zero divisor, then it is a unit.

Integral element of an algebra over artinian ring R is either a zero divisor or a unit.