opcyclesMap_neg

Mathlib.Algebra.Homology.ShortComplex.Preadditive

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.opcyclesMap_neg

English

For φ with data h1,h2, opcyclesMap'(-φ) h1 h2 = - opcyclesMap'(φ) h1 h2.

Русский

Для φ с данными h1,h2 операция opcyclesMap'(-φ) равна минусу opcyclesMap'(φ).

LaTeX

$$$\mathrm{opcyclesMap}'(-\varphi)\, h_1\, h_2 = -\mathrm{opcyclesMap}'(\varphi)\, h_1\, h_2$$$

Lean4

@[simp]
theorem opcyclesMap_neg : opcyclesMap (-φ) = -opcyclesMap φ :=
  opcyclesMap'_neg _ _

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

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

Разделы

Аффилиация

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