isArtinianRing — Mathlib

English

A ring is Artinian if and only if it is Artinian as a module over itself.

Русский

Кольцо артинаново тогда и только тогда, когда оно артинаново как R-модуль над самим кольцом.

LaTeX

$$$ IsArtinian\\; Ring\\; R \\iff IsArtinian\\; R\\; R. $$$

Lean4

theorem isArtinianRing {R} [Semiring R] {S} [Semiring S] {F} [FunLike F R S] [RingHomClass F R S] {f : F}
    (hf : Function.Surjective f) [H : IsArtinianRing R] : IsArtinianRing S :=
  by
  rw [isArtinianRing_iff] at H ⊢
  exact ⟨(Ideal.orderEmbeddingOfSurjective f hf).wellFounded H.wf⟩

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