isArtinianRing

Mathlib.RingTheory.Artinian.Module

URI: https://scilib.ai/kg/mathlib#RingEquiv.isArtinianRing

English

If R ≃+* S is a ring equivalence and R is Artinian, then S is Artinian.

Русский

Если существует эквивалентность колец R ≃+* S и R артинаново, то S артинаново.

LaTeX

$$$ (R\\simeq S) \\Rightarrow IsArtinianRing S \\leftarrow IsArtinianRing R. $$$

Lean4

theorem isArtinianRing {R S} [Semiring R] [Semiring S] (f : R ≃+* S) [IsArtinianRing R] : IsArtinianRing S :=
  f.surjective.isArtinianRing

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

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

Разделы

Аффилиация

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