isArtinianRing_rangeS

Mathlib.RingTheory.Artinian.Module

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

← MathLib Explorer

English

For a ring R, IsArtinianRing R is equivalent to IsArtinian R R.

Русский

Для кольца R равенство IsArtinianRing R эквивалентно IsArtinian R R.

LaTeX

$$$ IsArtinianRing R \\iff IsArtinian R R. $$$

Lean4

instance isArtinianRing_rangeS {R} [Semiring R] {S} [Semiring S] (f : R →+* S) [IsArtinianRing R] :
    IsArtinianRing f.rangeS :=
  f.rangeSRestrict_surjective.isArtinianRing

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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