single_neg

Mathlib.RingTheory.HahnSeries.Addition

URI: https://scilib.ai/kg/mathlib#HahnSeries.single_neg

English

The single term is compatible with negation: single a (-r) = - single a r.

Русский

Единичный член совместим с отрицанием: single a (-r) = - single a r.

LaTeX

$$$$ \operatorname{single} a (-r) = -\operatorname{single} a r. $$$$

Lean4

@[simp]
theorem single_neg (a : Γ) (r : R) : single a (-r) = -single a r :=
  map_neg (single.addMonoidHom a) _

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

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

Разделы

Аффилиация

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