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
@[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
theorem dvd_neg_of_dvd {α : Type u_1} [semigroup α] [has_distrib_neg α] {a b : α} (h : a ∣ b) :
a ∣ -b
source
theorem dvd_of_dvd_neg {α : Type u_1} [semigroup α] [has_distrib_neg α] {a b : α} (h : a ∣ -b) :
a ∣ b
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
theorem neg_dvd_of_dvd {α : Type u_1} [semigroup α] [has_distrib_neg α] {a b : α} (h : a ∣ b) :
-a ∣ b
source
theorem dvd_of_neg_dvd {α : Type u_1} [semigroup α] [has_distrib_neg α] {a b : α} (h : -a ∣ b) :
a ∣ 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 dvd_sub {α : Type u_1} [non_unital_ring α] {a b c : α} (h₁ : a ∣ b) (h₂ : a ∣ c) :
a ∣ b - c
source
theorem dvd_add_iff_left {α : Type u_1} [non_unital_ring α] {a b c : α} (h : a ∣ c) :
a ∣ b ↔ a ∣ b + c
source
theorem dvd_add_iff_right {α : Type u_1} [non_unital_ring α] {a b c : α} (h : a ∣ b) :
a ∣ c ↔ a ∣ b + c
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 commutative 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 commutative ring, a divides the sum 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 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
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