bot_smul

Mathlib.Algebra.Algebra.Operations

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

English

A dual property: the bottom submodule acted on by any submodule N yields ⊥: ⊥ • N = ⊥.

Русский

Симметричное свойство: нулевой подмодуль, действуемый над любым N, даёт ⊥: ⊥ • N = ⊥.

LaTeX

$$$ \\bot \\cdot N = \\bot $$$

Lean4

@[simp]
theorem bot_smul : (⊥ : Submodule R A) • N = ⊥ :=
  le_bot_iff.mp <| smul_le.mpr <| by rintro _ rfl _ _; rw [zero_smul]; exact zero_mem _

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

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

Разделы

Аффилиация

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