smul_set_neg

Mathlib.Algebra.Ring.Action.Pointwise.Set

URI: https://scilib.ai/kg/mathlib#Set.smul_set_neg

English

For a scalar a and a set t of a module, the smul of the negated set equals the negation of the smul: a • (-t) = -(a • t).

Русский

Для скаляра a и множества t модуля верно: a • (-t) = -(a • t).

LaTeX

$$$a \\cdot (-t) = -(a \\cdot t)$$$

Lean4

@[simp]
theorem smul_set_neg : a • -t = -(a • t) := by simp_rw [← image_smul, ← image_neg_eq_neg, image_image, smul_neg]

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

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

Разделы

Аффилиация

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