# mathlib3documentation

algebra.ring.divisibility

# Lemmas about divisibility in rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

theorem dvd_add {α : Type u_1} [has_add α] [semigroup α] {a b c : α} (h₁ : a b) (h₂ : a c) :
a b + c
theorem has_dvd.dvd.add {α : Type u_1} [has_add α] [semigroup α] {a b c : α} (h₁ : a b) (h₂ : a c) :
a b + c

Alias of dvd_add.

@[simp]
theorem two_dvd_bit0 {α : Type u_1} [semiring α] {a : α} :
2 bit0 a
theorem has_dvd.dvd.linear_comb {α : Type u_1} {d x y : α} (hdx : d x) (hdy : d y) (a b : α) :
d a * x + b * y
@[simp]
theorem dvd_neg {α : Type u_1} [semigroup α] {a b : α} :
a -b a b

An element a of a semigroup with a distributive negation divides the negation of an element b iff a divides b.

@[simp]
theorem neg_dvd {α : Type u_1} [semigroup α] {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.

theorem has_dvd.dvd.neg_left {α : Type u_1} [semigroup α] {a b : α} :
a b -a b

Alias of the reverse direction of neg_dvd.

theorem has_dvd.dvd.of_neg_left {α : Type u_1} [semigroup α] {a b : α} :
-a b a b

Alias of the forward direction of neg_dvd.

theorem has_dvd.dvd.neg_right {α : Type u_1} [semigroup α] {a b : α} :
a b a -b

Alias of the reverse direction of dvd_neg.

theorem has_dvd.dvd.of_neg_right {α : Type u_1} [semigroup α] {a b : α} :
a -b a b

Alias of the forward direction of dvd_neg.

theorem dvd_sub {α : Type u_1} {a b c : α} (h₁ : a b) (h₂ : a c) :
a b - c
theorem has_dvd.dvd.sub {α : Type u_1} {a b c : α} (h₁ : a b) (h₂ : a c) :
a b - c

Alias of dvd_sub.

theorem dvd_add_left {α : Type u_1} {a b c : α} (h : a c) :
a b + c a b

If an element a divides another element c in a ring, a divides the sum of another element b with c iff a divides b.

theorem dvd_add_right {α : Type u_1} {a b c : α} (h : a b) :
a b + c a c

If an element a divides another element b in a ring, a divides the sum of b and another element c iff a divides c.

theorem dvd_sub_left {α : Type u_1} {a b c : α} (h : a c) :
a b - c a b

If an element a divides another element c in a ring, a divides the difference of another element b with c iff a divides b.

theorem dvd_sub_right {α : Type u_1} {a b c : α} (h : a b) :
a b - c a c

If an element a divides another element b in a ring, a divides the difference of b and another element c iff a divides c.

theorem dvd_iff_dvd_of_dvd_sub {α : Type u_1} {a b c : α} (h : a b - c) :
a b a c
theorem dvd_sub_comm {α : Type u_1} {a b c : α} :
a b - c a c - b
theorem two_dvd_bit1 {α : Type u_1} [ring α] {a : α} :
2 bit1 a 2 1
@[simp]
theorem dvd_add_self_left {α : Type u_1} [ring α] {a b : α} :
a a + b a b

An element a divides the sum a + b if and only if a divides b.

@[simp]
theorem dvd_add_self_right {α : Type u_1} [ring α] {a b : α} :
a b + a a b

An element a divides the sum b + a if and only if a divides b.

@[simp]
theorem dvd_sub_self_left {α : Type u_1} [ring α] {a b : α} :
a a - b a b

An element a divides the difference a - b if and only if a divides b.

@[simp]
theorem dvd_sub_self_right {α : Type u_1} [ring α] {a b : α} :
a b - a a b

An element a divides the difference b - a if and only if a divides b.

theorem dvd_mul_sub_mul {α : Type u_1} {k a b x y : α} (hab : k a - b) (hxy : k x - y) :
k a * x - b * y