Associated elements in rings

theorem Associated.neg_left {M : Type u_1} [Monoid M] [HasDistribNeg M] {a b : M} (h : Associated a b) : Associated (-a) b

theorem Associated.neg_right {M : Type u_1} [Monoid M] [HasDistribNeg M] {a b : M} (h : Associated a b) : Associated a (-b)

theorem Associated.neg_neg {M : Type u_1} [Monoid M] [HasDistribNeg M] {a b : M} (h : Associated a b) : Associated (-a) (-b)

@[simp]

theorem Associated.neg_left_iff {M : Type u_1} [Monoid M] [HasDistribNeg M] {a b : M} : Associated (-a) b ↔ Associated a b

@[simp]

theorem Associated.neg_right_iff {M : Type u_1} [Monoid M] [HasDistribNeg M] {a b : M} : Associated a (-b) ↔ Associated a b