sym_neg

Mathlib.Algebra.Symmetrized

URI: https://scilib.ai/kg/mathlib#SymAlg.sym_neg

English

For α with Neg, sym(-a) = -sym(a).

Русский

Для α с операцией отрицания, sym(-a) = -sym(a).

LaTeX

$$$\forall \{\alpha\} [\text{Neg } \alpha] (a : \alpha),\ sym(-a) = -\operatorname{sym}(a)$$$

Lean4

@[simp]
theorem sym_neg [Neg α] (a : α) : sym (-a) = -sym a :=
  rfl

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

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

Разделы

Аффилиация

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