smul_bot

Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise

URI: https://scilib.ai/kg/mathlib#AddSubmonoid.smul_bot

English

The image of the bottom submonoid under any action is the bottom submonoid: m • ⊥ = ⊥.

Русский

Образ нулевого подмножества под действием любого m равен нулевому подмножеству: m • ⊥ = ⊥.

LaTeX

$$$ m \cdot (\perp) = (\perp) $$$

Lean4

@[simp]
theorem smul_bot (m : M) : m • (⊥ : AddSubmonoid A) = ⊥ :=
  map_bot _

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

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

Разделы

Аффилиация

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