mul_bot

Mathlib.Algebra.Algebra.Operations

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

English

The product with the bottom submodule yields bottom: ⊥ * M = ⊥.

Русский

Произведение с нулевым подмодулем дает нулевой: ⊥ * M = ⊥.

LaTeX

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

Lean4

@[simp]
theorem mul_bot : M * ⊥ = ⊥ :=
  smul_bot _

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

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

Разделы

Аффилиация

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