Lemmas about divisibility in rings #

theorem dvd_add {α : Type u_1} [inst : Add α] [inst : Semigroup α] [inst : LeftDistribClass α] {a : α} {b : α} {c : α} (h₁ : a ∣ b) (h₂ : a ∣ c) :

a ∣ b + c

source

ink

@[simp]

theorem two_dvd_bit0 {α : Type u_1} [inst : Semiring α] {a : α} :

2 ∣ bit0 a

source

ink

theorem Dvd.dvd.linear_comb {α : Type u_1} [inst : NonUnitalCommSemiring α] {d : α} {x : α} {y : α} (hdx : d ∣ x) (hdy : d ∣ y) (a : α) (b : α) :

d ∣ a * x + b * y

source

ink

theorem dvd_neg_of_dvd {α : Type u_1} [inst : Semigroup α] [inst : HasDistribNeg α] {a : α} {b : α} (h : a ∣ b) :

a ∣ -b

source

ink

theorem dvd_of_dvd_neg {α : Type u_1} [inst : Semigroup α] [inst : HasDistribNeg α] {a : α} {b : α} (h : a ∣ -b) :

a ∣ b

source

ink

@[simp]

theorem dvd_neg {α : Type u_1} [inst : Semigroup α] [inst : HasDistribNeg α] (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

ink

theorem neg_dvd_of_dvd {α : Type u_1} [inst : Semigroup α] [inst : HasDistribNeg α] {a : α} {b : α} (h : a ∣ b) :

-a ∣ b

source

ink

theorem dvd_of_neg_dvd {α : Type u_1} [inst : Semigroup α] [inst : HasDistribNeg α] {a : α} {b : α} (h : -a ∣ b) :

a ∣ b

source

ink

@[simp]

theorem neg_dvd {α : Type u_1} [inst : Semigroup α] [inst : HasDistribNeg α] (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

ink

theorem dvd_sub {α : Type u_1} [inst : NonUnitalRing α] {a : α} {b : α} {c : α} (h₁ : a ∣ b) (h₂ : a ∣ c) :

a ∣ b - c

source

ink

theorem dvd_add_iff_left {α : Type u_1} [inst : NonUnitalRing α] {a : α} {b : α} {c : α} (h : a ∣ c) :

a ∣ b ↔ a ∣ b + c

source

ink

theorem dvd_add_iff_right {α : Type u_1} [inst : NonUnitalRing α] {a : α} {b : α} {c : α} (h : a ∣ b) :

a ∣ c ↔ a ∣ b + c

source

ink

theorem dvd_add_left {α : Type u_1} [inst : NonUnitalRing α] {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

ink

theorem dvd_add_right {α : Type u_1} [inst : NonUnitalRing α] {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

ink

theorem dvd_iff_dvd_of_dvd_sub {α : Type u_1} [inst : NonUnitalRing α] {a : α} {b : α} {c : α} (h : a ∣ b - c) :

a ∣ b ↔ a ∣ c

source

ink

theorem two_dvd_bit1 {α : Type u_1} [inst : Ring α] {a : α} :

2 ∣ bit1 a ↔ 2 ∣ 1

source

ink

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

source

ink

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

source

ink

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

k ∣ a * x - b * y