smulWithZero

Mathlib.Algebra.GroupWithZero.Action.Prod

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

← MathLib Explorer

English

The product M × N inherits a MulActionWithZero structure: a • 0 = 0.

Русский

Произведение M × N наследует MulActionWithZero: a • 0 = 0.

LaTeX

$$$a \\cdot (0,0) = (0,0)$$$

Lean4

instance smulWithZero {R : Type*} [Zero R] [Zero M] [Zero N] [SMulWithZero R M] [SMulWithZero R N] :
    SMulWithZero R (M × N) where zero_smul _ := by ext <;> exact zero_smul ..

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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