Lemmas about divisibility in rings

Note that this file is imported by basic tactics like linarith and so must have only minimal imports. Further results about divisibility in rings may be found in Mathlib/Algebra/Ring/Divisibility/Lemmas.lean which is not subject to this import constraint.

theorem map_dvd_iff {α : Type u_1} {β : Type u_2} [Semigroup α] [Semigroup β] {F : Type u_3} [EquivLike F α β] [MulEquivClass F α β] (f : F) {a b : α} : f a ∣ f b ↔ a ∣ b

theorem map_dvd_iff_dvd_symm {α : Type u_1} {β : Type u_2} [Semigroup α] [Semigroup β] {F : Type u_3} [EquivLike F α β] [MulEquivClass F α β] (f : F) {a : α} {b : β} : f a ∣ b ↔ a ∣ (↑f).symm b

theorem MulEquiv.decompositionMonoid {α : Type u_1} {β : Type u_2} [Semigroup α] [Semigroup β] {F : Type u_3} [EquivLike F α β] [MulEquivClass F α β] (f : F) [DecompositionMonoid β] : DecompositionMonoid α

noncomputable def Equiv.dvd {G : Type u_4} [LeftCancelSemigroup G] (g : G) : G ≃ { a : G // g ∣ a }

If G is a LeftCancelSemiGroup, left multiplication by g yields an equivalence between G and the set of elements of G divisible by g.

Equations

• Equiv.dvd g = { toFun := fun (a : G) => ⟨g * a, ⋯⟩, invFun := fun (x : { a : G // g ∣ a }) => match x with | ⟨val, h⟩ => Exists.choose h, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.dvd_apply {G : Type u_4} [LeftCancelSemigroup G] (g a : G) : ↑((Equiv.dvd g) a) = g * a

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

theorem Dvd.dvd.add {α : Type u_1} [Add α] [Semigroup α] [LeftDistribClass α] {a b c : α} (h₁ : a ∣ b) (h₂ : a ∣ c) : a ∣ b + c

Alias of dvd_add.

theorem min_pow_dvd_add {α : Type u_1} [Semiring α] {a b c : α} {m n : ℕ} (ha : c ^ m ∣ a) (hb : c ^ n ∣ b) : c ^ min m n ∣ a + b

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

@[simp]

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

@[simp]

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

theorem Dvd.dvd.neg_left {α : Type u_1} [Semigroup α] [HasDistribNeg α] {a b : α} : a ∣ b → -a ∣ b

Alias of the reverse direction of neg_dvd.

---

The negation of an element a of a semigroup with a distributive negation divides another element b iff a divides b.

theorem Dvd.dvd.of_neg_left {α : Type u_1} [Semigroup α] [HasDistribNeg α] {a b : α} : -a ∣ b → a ∣ b

Alias of the forward direction of neg_dvd.

---

The negation of an element a of a semigroup with a distributive negation divides another element b iff a divides b.

theorem Dvd.dvd.of_neg_right {α : Type u_1} [Semigroup α] [HasDistribNeg α] {a b : α} : a ∣ -b → a ∣ b

Alias of the forward direction of dvd_neg.

---

An element a of a semigroup with a distributive negation divides the negation of an element b iff a divides b.

theorem Dvd.dvd.neg_right {α : Type u_1} [Semigroup α] [HasDistribNeg α] {a b : α} : a ∣ b → a ∣ -b

Alias of the reverse direction of dvd_neg.

---

An element a of a semigroup with a distributive negation divides the negation of an element b iff a divides b.

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

theorem Dvd.dvd.sub {α : Type u_1} [NonUnitalRing α] {a b c : α} (h₁ : a ∣ b) (h₂ : a ∣ c) : a ∣ b - c

Alias of dvd_sub.

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

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

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

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

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

theorem dvd_sub_comm {α : Type u_1} [NonUnitalRing α] {a b c : α} : a ∣ b - c ↔ a ∣ c - b

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

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

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

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