finite_iff_isArtinianRing — Mathlib

English

If R is Artinian and A is Artinian, then A is finite over R iff A is Artinian.

Русский

Если R артин, и A артин, то A конечна над R тогда и только тогда A артин.

LaTeX

$$Module.finite_iff_isArtinianRing$$

Lean4

/-- If `A` is a finite type algebra over an Artinian ring `R`,
then `A` is finite over `R` if and only if `A` is an Artinian ring. -/
theorem finite_iff_isArtinianRing [IsArtinianRing R] : Module.Finite R A ↔ IsArtinianRing A :=
  ⟨isArtinian_of_tower _ ∘ ((IsArtinianRing.tfae R A).out 0 2).mp, fun _ ↦ finite_of_isArtinianRing R A⟩

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