instIsCocomm

Mathlib.RingTheory.Coalgebra.MonoidAlgebra

URI: https://scilib.ai/kg/mathlib#AddMonoidAlgebra.instIsCocomm

English

If A is cocommutative, then AddMonoidAlgebra A X is cocommutative.

Русский

Если A ко-коммутативна, то AddMonoidAlgebra A X ко-коммутативна.

LaTeX

$$$\text{IsCocomm}(R, A[X])$ given $\text{IsCocomm}(R,A)$$$

Lean4

instance instIsCocomm [IsCocomm R A] : IsCocomm R A[X] :=
  Finsupp.instIsCocomm R X A

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

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

Разделы

Аффилиация

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