single_neg

Mathlib.Data.DFinsupp.Defs

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

English

For AddGroup, single i (−x) = − single i x.

Русский

Для группы сложения единичная функция сохраняет минус: single i (−x) = − single i x.

LaTeX

$$$ \\mathrm{single}_i (-x) = -\\mathrm{single}_i x $$$

Lean4

@[simp]
theorem single_neg {β : ι → Type v} [∀ i, AddGroup (β i)] (i : ι) (x : β i) : single i (-x) = -single i x :=
  (singleAddHom β i).map_neg x

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

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

Разделы

Аффилиация

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