Theorems · Theorem · commutative algebra

Dvd.dvd.neg_right

∀ {α : Type u_1} [inst : Semigroup α] [inst_1 : HasDistribNeg α] {a b : α}, a ∣ b → a ∣ -b

Alias of the reverse direction of dvd_neg. An element a of a semigroup with a distributive negation divides the negation of an element b iff a divides b.

Defined in

Mathlib.Algebra.Ring.Divisibility.Basic

Cited by

5 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext, Quot.sound

Assumes

SemigroupHasDistribNeg