instMul

Mathlib.RingTheory.PiTensorProduct

URI: https://scilib.ai/kg/mathlib#PiTensorProduct.instMul

English

There is a canonical multiplication on the PiTensorProduct given by coordinatewise multiplication.

Русский

Существует каноническое умножение на PiTensorProduct, задаваемое покоординатно умножением.

LaTeX

$$mul : (⨂[R] i, A i) → (⨂[R] i, A i) → (⨂[R] i, A i) with mul x y := mul x y$$

Lean4

instance instMul : Mul (⨂[R] i, A i) where mul x y := mul x y

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

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

Разделы

Аффилиация

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