zero_mul

Mathlib.Data.Holor

URI: https://scilib.ai/kg/mathlib#Holor.zero_mul

← MathLib Explorer

English

Left zero multiplication: the zero holor annihilates any holor on the left: 0 ⊗ x = 0.

Русский

Левое умножение на нуль даёт нуль: 0 ⊗ x = 0.

LaTeX

$$0 \otimes x = 0$$

Lean4

@[simp]
nonrec theorem zero_mul {α : Type} [MulZeroClass α] (x : Holor α ds₂) : (0 : Holor α ds₁) ⊗ x = 0 :=
  funext fun t => zero_mul (x (HolorIndex.drop t))

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

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

Разделы

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

Аффилиация

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