isSupported_neg

Mathlib.RingTheory.FreeCommRing

URI: https://scilib.ai/kg/mathlib#FreeCommRing.isSupported_neg

English

If x is supported on s, then −x is also supported on s.

Русский

Если x поддержано на s, то −x тоже поддержано на s.

LaTeX

$$$ (\\text{IsSupported}\\, x\\, s) \\Rightarrow \\text{IsSupported}(-x, s) $$$

Lean4

theorem isSupported_neg (hxs : IsSupported x s) : IsSupported (-x) s :=
  Subring.neg_mem _ hxs

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

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

Разделы

Аффилиация

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