smul_mk_zero

Mathlib.Algebra.GroupWithZero.Action.Prod

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

← MathLib Explorer

English

Let a ∈ M and b ∈ α. Then a · (b, 0) = (a · b, 0).

Русский

Пусть a ∈ M и b ∈ α. Тогда a · (b, 0) = (a · b, 0).

LaTeX

$$$a \\cdot (b, (0 : \\beta)) = (a \\cdot b, 0)$$$

Lean4

theorem smul_mk_zero {β : Type*} [Monoid M] [AddMonoid β] [DistribMulAction M β] (a : M) (b : α) :
    a • (b, (0 : β)) = (a • b, 0) := by rw [Prod.smul_mk, smul_zero]

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

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

Разделы

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

Аффилиация

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