instDecompositionMonoid

Mathlib.RingTheory.Artinian.Instances

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

English

Over an Artinian ring R, the polynomial ring R[X] inherits a decomposition monoid structure.

Русский

Над Artinian-кольцом R, кольцо многочленов R[X] наследует структуру декомпозиционного моноида.

LaTeX

$$$\\text{IsArtinianRing } R \\Rightarrow \\text{DecompositionMonoid}(\\text{Polynomial } R)$$$

Lean4

instance : DecompositionMonoid R :=
  MulEquiv.decompositionMonoid (equivPi R)

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

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

Разделы

Аффилиация

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