comul_comp_inl

Mathlib.RingTheory.Coalgebra.Basic

URI: https://scilib.ai/kg/mathlib#Prod.comul_comp_inl

English

The product coalgebra inherits cocommutativity componentwise.

Русский

Произведение коалгебра получает кококоммутативность по компонентам.

LaTeX

$$$\\text{Prod.IsCocomm}$$$

Lean4

theorem comul_comp_inl : comul ∘ₗ inl R A B = TensorProduct.map (.inl R A B) (.inl R A B) ∘ₗ comul := by ext; simp

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

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

Разделы

Аффилиация

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