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.

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

Alias of dvd_add.

source
@[simp]
theorem two_dvd_bit0 {α : Type u_1} [semiring α] {a : α} :
2 ∣ bit0 a
source
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
source
@[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.

source
@[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.

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

Alias of the reverse direction of neg_dvd.

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

Alias of the forward direction of neg_dvd.

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

Alias of the reverse direction of dvd_neg.

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

Alias of the forward direction of dvd_neg.

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

Alias of dvd_sub.

source
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 ring, a divides the sum of another element b with c iff a divides b.

source
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 ring, a divides the sum of b and another element c iff a divides c.

source
theorem dvd_sub_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 ring, a divides the difference of another element b with c iff a divides b.

source
theorem dvd_sub_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 ring, a divides the difference of b and another element c iff a divides c.

source
theorem dvd_iff_dvd_of_dvd_sub {α : Type u_1} [non_unital_ring α] {a b c : α} (h : a ∣ b - c) :
a ∣ b ↔ a ∣ c
source
theorem dvd_sub_comm {α : Type u_1} [non_unital_ring α] {a b c : α} :
a ∣ b - c ↔ a ∣ c - b
source
theorem two_dvd_bit1 {α : Type u_1} [ring α] {a : α} :
2 ∣ bit1 a ↔ 2 ∣ 1
source
@[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.

source
@[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.

source
@[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.

source
@[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.

source
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