support_neg

Mathlib.Algebra.SkewMonoidAlgebra.Support

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

← MathLib Explorer

English

Taking formal additive inverses does not change the support.

Русский

Взятие формального сложения с противоположным не изменяет опору.

LaTeX

$$$( -p).\\operatorname{support} = p.\\operatorname{support}$$$

Lean4

theorem support_neg (p : SkewMonoidAlgebra k G) : (-p).support = p.support := by
  rw [support, toFinsupp_neg, Finsupp.support_neg, support_toFinsupp]

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

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

Разделы

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

Аффилиация

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