localization_artinian

Mathlib.RingTheory.Artinian.Ring

URI: https://scilib.ai/kg/mathlib#IsArtinianRing.localization_artinian

English

Localizing an Artinian ring yields an Artinian ring.

Русский

Локализация артинианова кольца даёт артинианово кольцо.

LaTeX

$$$IsArtinianRing\ L$$$

Lean4

theorem localization_artinian : IsArtinianRing L :=
  (localization_surjective S L).isArtinianRing

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

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

Разделы

Аффилиация

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