smul_neg

Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset

URI: https://scilib.ai/kg/mathlib#Finset.smul_neg

← MathLib Explorer

English

Smul distributes over negation: s · (-t) = -(s · t).

Русский

Умножение распределяется над отрицанием: s · (-t) = -(s · t).

LaTeX

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

Lean4

@[simp]
protected theorem smul_neg (s : Finset α) (t : Finset β) : s • -t = -(s • t) := by simp_rw [← image_neg_eq_neg];
  exact image_image₂_right_comm smul_neg

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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