isUnit_of_nonZeroDivisor_of_isIntegral'

English

If s ≤ t are submodules of M and t is Artinian over R, then s is Artinian over R.

Русский

Если s ≤ t — подмодуля M и t артинарен над R, то s тоже артинарен над R.

LaTeX

$$$\\forall s,t \\le M:\\; s \\le t \\Rightarrow \\mathrm{IsArtinian}_R(t) \\Rightarrow \\mathrm{IsArtinian}_R(s)$$$

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_nonZeroDivisor_of_isIntegral' [Algebra.IsIntegral R A] {a : A} (ha : a ∈ A⁰) : IsUnit a :=
  isUnit_of_isIntegral_of_nonZeroDivisor (R := R) (Algebra.IsIntegral.isIntegral a) ha

Похожие утверждения