single_neg — Mathlib

English

The singleton at a with -b equals the negation of the singleton at a with b: single a (-b) = - single a b.

Русский

Одиночный элемент на позиции a с значением -b равен отрицанию одиночного элемента на позиции a сb: single a (-b) = - single a b.

LaTeX

$$$\mathrm{single}(a, -b) = -\mathrm{single}(a, b)$$$

Lean4

@[simp]
theorem single_neg (a : ι) (b : G) : single a (-b) = -single a b :=
  (singleAddHom a : G →+ _).map_neg b

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