isArtinianRing_iff

Mathlib.RingTheory.Artinian.Module

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

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

theorem isArtinianRing_iff {R} [Semiring R] : IsArtinianRing R ↔ IsArtinian R R :=
  Iff.rfl

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

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

Разделы

Аффилиация

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