isArtinianRing_range

Mathlib.RingTheory.Artinian.Module

URI: https://scilib.ai/kg/mathlib#isArtinianRing_range

English

If f : R →+* S with R Artinian, then the range ring f.rangeS is Artinian.

Русский

Если f : R →+* S и R артинаново, то диапазонный кольцо f.rangeS артинаново.

LaTeX

$$$ IsArtinianRing R \\Rightarrow IsArtinianRing f.rangeS. $$$

Lean4

instance isArtinianRing_range {R} [Ring R] {S} [Ring S] (f : R →+* S) [IsArtinianRing R] : IsArtinianRing f.range :=
  isArtinianRing_rangeS f

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru