support_neg

Mathlib.Algebra.FreeAbelianGroup.Finsupp

URI: https://scilib.ai/kg/mathlib#FreeAbelianGroup.support_neg

← MathLib Explorer

English

Taking additive inverses does not change the support.

Русский

При взятии противоположного по сложению поддержка не меняется.

LaTeX

$$$\\operatorname{support}(-a) = \\operatorname{support}(a)$$$

Lean4

@[simp]
theorem support_neg (a : FreeAbelianGroup X) : support (-a) = support a := by
  simp only [support, AddMonoidHom.map_neg, Finsupp.support_neg]

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

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

Разделы

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

Аффилиация

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