instIsArtinianRingProd

Mathlib.RingTheory.Artinian.Module

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

← MathLib Explorer

English

The product of two Artinian rings is Artinian.

Русский

Произведение (продукт) двух артинанных колец является артинановым.

LaTeX

$$$ IsArtinianRing R \\Rightarrow IsArtinianRing S \\Rightarrow IsArtinianRing (R \\times S). $$$

Lean4

instance {R S} [Semiring R] [Semiring S] [IsArtinianRing R] [IsArtinianRing S] : IsArtinianRing (R × S) :=
  Ideal.idealProdEquiv.toOrderEmbedding.wellFoundedLT

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

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

Разделы

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

Аффилиация

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