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] [CommRing 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] [CommRing 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] [CommRing 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] [CommRing 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] [CommRing A] [Algebra R A] [Algebra.IsIntegral R A] : IsUnit.submonoid A = nonZeroDivisors A