bot_mul

Mathlib.Algebra.Algebra.Operations

URI: https://scilib.ai/kg/mathlib#Submodule.bot_mul

English

Similarly, M * ⊥ = ⊥.

Русский

Аналогично, M * ⊥ = ⊥.

LaTeX

$$$ M \cdot \bot = \bot $$$

Lean4

@[simp]
theorem bot_mul : ⊥ * M = ⊥ :=
  bot_smul _

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

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

Разделы

Аффилиация

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