Algebras over Artinian rings

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

theorem IsArtinianRing.isUnit_of_isIntegral_of_nonZeroDivisor {R : Type u_1} {A : Type u_2} [CommRing R] [IsArtinianRing R] [Ring A] [Algebra R A] {a : A} (hi : IsIntegral R a) (ha : a ∈ nonZeroDivisors A) : IsUnit a

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.

theorem IsArtinianRing.isUnit_iff_nonZeroDivisor_of_isIntegral {R : Type u_1} {A : Type u_2} [CommRing R] [IsArtinianRing R] [Ring A] [Algebra R A] {a : A} (hi : IsIntegral R a) : IsUnit a ↔ a ∈ nonZeroDivisors A

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

theorem IsArtinianRing.isUnit_of_nonZeroDivisor_of_isIntegral' {R : Type u_1} {A : Type u_2} [CommRing R] [IsArtinianRing R] [Ring A] [Algebra R A] [Algebra.IsIntegral R A] {a : A} (ha : a ∈ nonZeroDivisors A) : IsUnit a

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.

theorem IsArtinianRing.isUnit_iff_nonZeroDivisor_of_isIntegral' {R : Type u_1} {A : Type u_2} [CommRing R] [IsArtinianRing R] [Ring A] [Algebra R A] [Algebra.IsIntegral R A] {a : A} : IsUnit a ↔ a ∈ nonZeroDivisors A

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

theorem IsArtinianRing.isUnit_submonoid_eq_of_isIntegral {R : Type u_1} {A : Type u_2} [CommRing R] [IsArtinianRing R] [Ring A] [Algebra R A] [Algebra.IsIntegral R A] : IsUnit.submonoid A = nonZeroDivisors A