neg_right_iff — Mathlib

English

Negating the right argument preserves associativity; i.e., associated a (-b) iff associated a b.

Русский

Устойчивость по правому аргументу: a ассоциировано с -b тогда и только тогда, когда a ассоциировано с b.

LaTeX

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

Lean4

@[simp]
theorem neg_right_iff : Associated a (-b) ↔ Associated a b :=
  ⟨fun h ↦ _root_.neg_neg b ▸ h.neg_right, fun h ↦ h.neg_right⟩

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