# Associated elements in rings #

source
theorem Associated.neg_left {M : Type u_1} [Monoid M] [HasDistribNeg M] {a b : M} (h : Associated a b) :
Associated (-a) b
source
theorem Associated.neg_right {M : Type u_1} [Monoid M] [HasDistribNeg M] {a b : M} (h : Associated a b) :
Associated a (-b)
source
theorem Associated.neg_neg {M : Type u_1} [Monoid M] [HasDistribNeg M] {a b : M} (h : Associated a b) :
Associated (-a) (-b)
source
@[simp]
theorem Associated.neg_left_iff {M : Type u_1} [Monoid M] [HasDistribNeg M] {a b : M} :
Associated (-a) b ↔ Associated a b
source
@[simp]
theorem Associated.neg_right_iff {M : Type u_1} [Monoid M] [HasDistribNeg M] {a b : M} :
Associated a (-b) ↔ Associated a b