# Documentation

Mathlib.Algebra.Ring.Divisibility

# Lemmas about divisibility in rings #

theorem dvd_add {α : Type u_1} [inst : Add α] [inst : ] [inst : ] {a : α} {b : α} {c : α} (h₁ : a b) (h₂ : a c) :
a b + c
@[simp]
theorem two_dvd_bit0 {α : Type u_1} [inst : ] {a : α} :
2 bit0 a
theorem Dvd.dvd.linear_comb {α : Type u_1} [inst : ] {d : α} {x : α} {y : α} (hdx : d x) (hdy : d y) (a : α) (b : α) :
d a * x + b * y
theorem dvd_neg_of_dvd {α : Type u_1} [inst : ] [inst : ] {a : α} {b : α} (h : a b) :
a -b
theorem dvd_of_dvd_neg {α : Type u_1} [inst : ] [inst : ] {a : α} {b : α} (h : a -b) :
a b
@[simp]
theorem dvd_neg {α : Type u_1} [inst : ] [inst : ] (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.

theorem neg_dvd_of_dvd {α : Type u_1} [inst : ] [inst : ] {a : α} {b : α} (h : a b) :
-a b
theorem dvd_of_neg_dvd {α : Type u_1} [inst : ] [inst : ] {a : α} {b : α} (h : -a b) :
a b
@[simp]
theorem neg_dvd {α : Type u_1} [inst : ] [inst : ] (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 dvd_sub {α : Type u_1} [inst : ] {a : α} {b : α} {c : α} (h₁ : a b) (h₂ : a c) :
a b - c
theorem dvd_add_iff_left {α : Type u_1} [inst : ] {a : α} {b : α} {c : α} (h : a c) :
a b a b + c
theorem dvd_add_iff_right {α : Type u_1} [inst : ] {a : α} {b : α} {c : α} (h : a b) :
a c a b + c
theorem dvd_add_left {α : Type u_1} [inst : ] {a : α} {b : α} {c : α} (h : a c) :
a b + c a b

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

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

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

theorem dvd_iff_dvd_of_dvd_sub {α : Type u_1} [inst : ] {a : α} {b : α} {c : α} (h : a b - c) :
a b a c
theorem two_dvd_bit1 {α : Type u_1} [inst : Ring α] {a : α} :
2 bit1 a 2 1
@[simp]
theorem dvd_add_self_left {α : Type u_1} [inst : 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} [inst : Ring α] {a : α} {b : α} :
a b + a a b

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

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