Mathlib.Algebra.Ring.Associated

Associated.neg_left theorem

(h : Associated a b) : Associated (-a) b

Full source

lemma neg_left (h : Associated a b) : Associated (-a) b := let ⟨u, hu⟩ := h; ⟨-u, by simp [hu]⟩

Negation Preserves Association: $-a \sim b$ given $a \sim b$

Informal description

If two elements $a$ and $b$ in a monoid $M$ are associated (i.e., there exists a unit $u$ such that $a \cdot u = b$), then $-a$ and $b$ are also associated.

Associated.neg_right theorem

(h : Associated a b) : Associated a (-b)

Full source

lemma neg_right (h : Associated a b) : Associated a (-b) := h.symm.neg_left.symm

Negation Preserves Association: $a \sim -b$ given $a \sim b$

Informal description

For any elements $a$ and $b$ in a monoid $M$ with distributive negation, if $a$ and $b$ are associated (i.e., there exists a unit $u$ such that $a \cdot u = b$), then $a$ and $-b$ are also associated.

Associated.neg_neg theorem

(h : Associated a b) : Associated (-a) (-b)

Full source

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

Negation Preserves Association: $-a \sim -b$ given $a \sim b$

Informal description

For any elements $a$ and $b$ in a monoid $M$ with distributive negation, if $a$ and $b$ are associated (i.e., $a \sim b$), then $-a$ and $-b$ are also associated (i.e., $-a \sim -b$).