Theorems · Theorem · commutative algebra

neg_dvd

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

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

3 results in Mathlib

Foundations

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

Assumes

SemigroupHasDistribNeg