Theorems · Theorem · commutative algebra

IsArtinianRing.isUnit_of_isIntegral_of_nonZeroDivisor

∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [IsArtinianRing R] [inst_2 : Ring A] [inst_3 : Algebra R A] {a : A},
  IsIntegral R a → 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.

Defined in

Mathlib.RingTheory.Artinian.Algebra

Cited by

2 results in Mathlib

Foundations

Depth 123 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsArtinianRingRingAlgebra