mathlib documentation

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 α] [left_distrib_class α] {a b c : α} (h₁ : a b) (h₂ : a c) :
a b + c
@[simp]
theorem two_dvd_bit0 {α : Type u_1} [semiring α] {a : α} :
2 bit0 a
theorem has_dvd.dvd.linear_comb {α : Type u_1} [non_unital_comm_semiring α] {d x y : α} (hdx : d x) (hdy : d y) (a b : α) :
d a * x + b * y
theorem dvd_neg_of_dvd {α : Type u_1} [semigroup α] [has_distrib_neg α] {a b : α} (h : a b) :
a -b
theorem dvd_of_dvd_neg {α : Type u_1} [semigroup α] [has_distrib_neg α] {a b : α} (h : a -b) :
a b
@[simp]
theorem dvd_neg {α : Type u_1} [semigroup α] [has_distrib_neg α] (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} [semigroup α] [has_distrib_neg α] {a b : α} (h : a b) :
-a b
theorem dvd_of_neg_dvd {α : Type u_1} [semigroup α] [has_distrib_neg α] {a b : α} (h : -a b) :
a b
@[simp]
theorem neg_dvd {α : Type u_1} [semigroup α] [has_distrib_neg α] (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} [non_unital_ring α] {a b c : α} (h₁ : a b) (h₂ : a c) :
a b - c
theorem dvd_add_iff_left {α : Type u_1} [non_unital_ring α] {a b c : α} (h : a c) :
a b a b + c
theorem dvd_add_iff_right {α : Type u_1} [non_unital_ring α] {a b c : α} (h : a b) :
a c a b + c
theorem dvd_add_left {α : Type u_1} [non_unital_ring α] {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} [non_unital_ring α] {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} [non_unital_ring α] {a b c : α} (h : a b - c) :
a b a c
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.

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