English
In an R-algebra, if a is integral over R and not a zero divisor, then a is a unit.
Русский
В R-алгебре, если a интегральен над R и не является нулевым делителем, то он является единицей.
LaTeX
$$$\\mathrm{IsIntegral}_R(a) \\land a \\in A^\\circ \\;\Rightarrow\; a \\text{ is a unit}$$$
Lean4
/-- 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 isUnit_of_isIntegral_of_nonZeroDivisor {a : A} (hi : IsIntegral R a) (ha : a ∈ A⁰) : IsUnit a :=
let B := Algebra.adjoin R { a }
let b : B := ⟨a, Algebra.self_mem_adjoin_singleton R a⟩
haveI : Module.Finite R B := Algebra.finite_adjoin_simple_of_isIntegral hi
haveI : IsArtinianRing B := isArtinian_of_tower R inferInstance
have hinj : Function.Injective B.subtype := Subtype.val_injective
have hb : b ∈ B⁰ := comap_nonZeroDivisors_le_of_injective hinj ha
(isUnit_of_mem_nonZeroDivisors hb).map B.subtype
