neg_left_iff — Mathlib

English

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

Русский

Упорядочение слева при отрицании сохраняет ассоциативность; то есть a и -a эквивалентны по ассоциации.

LaTeX

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

Lean4

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

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