neg_neg

Mathlib.Algebra.Ring.Associated

URI: https://scilib.ai/kg/mathlib#Associated.neg_neg

English

If a is associated to b, then -a is associated to -b (negation preserves associativity pairwise).

Русский

Если a ассоциировано с b, то -a ассоциировано с -b (сохранение ассоциативности через отрицание).

LaTeX

$$$\\text{Associated}(a,b) \\Rightarrow \\text{Associated}(-a,-b)$$$

Lean4

theorem neg_neg (h : Associated a b) : Associated (-a) (-b) :=
  h.neg_left.neg_right

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

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

Разделы

Аффилиация

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