Theorems · Theorem · commutative algebra

Dvd.dvd.neg_left

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

Alias of the reverse direction of neg_dvd. The negation of an element a of a semigroup with a distributive negation divides another element b iff a divides b.

Defined in: Mathlib.Algebra.Ring.Divisibility.Basic
Cited by: 0 results in Mathlib
Foundations: Depth 18 from the axioms · uses propext, Quot.sound
Assumes: Semigroup HasDistribNeg

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Semigroupstatement and proof · cited by 202
HasDistribNegstatement and proof · cited by 114
neg_dvdproof · cited by 3

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.