zero_smul

Mathlib.Algebra.Ring.Subgroup

URI: https://scilib.ai/kg/mathlib#AddSubgroup.zero_smul

English

In a module over a semiring, the zero scalar acting on any additive subgroup yields the bottom subgroup.

Русский

В модуле над полукольцом нулевой скаляр действует на любую сумму подгруппу как ноль: 0 • s = ⊥.

LaTeX

$$$ (0 : R) • s = \bot $$$

Lean4

@[simp]
protected theorem zero_smul (s : AddSubgroup M) : (0 : R) • s = ⊥ := by simp [eq_bot_iff_forall, pointwise_smul_def]

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

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

Разделы

Аффилиация

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