instIsArtinianRing

Mathlib.RingTheory.Artinian.Module

URI: https://scilib.ai/kg/mathlib#DivisionSemiring.instIsArtinianRing

English

Every DivisionSemiring is Artinian as a ring.

Русский

Любой DivisionSemiring является артинановым кольцом.

LaTeX

$$$ IsArtinianRing\\; K. $$$

Lean4

instance instIsArtinianRing {K : Type*} [DivisionSemiring K] : IsArtinianRing K :=
  ⟨Finite.wellFounded_of_trans_of_irrefl _⟩

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

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

Разделы

Аффилиация

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