Documentation

Mathlib.Algebra.Ring.Associated

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)