neg_smul

Mathlib.Algebra.Ring.Action.Pointwise.Set

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

English

In Set-wise smul with negation, one has the identity: Set.neg.neg s acts as the negation of the smul: (−s) • t = −(s • t).

Русский

В наборном smul с отрицанием имеет место равенство: (−s) • t = −(s • t).

LaTeX

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

Lean4

@[simp]
protected theorem neg_smul : -s • t = -(s • t) :=
  by
  simp_rw [← image_neg_eq_neg]
  exact image2_image_left_comm neg_smul

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

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

Разделы

Аффилиация

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