Documentation

Mathlib.Algebra.Ring.Divisibility.Basic

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 which is not subject to this import constraint.

source
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
source
theorem MulEquiv.decompositionMonoid {α : Type u_1} {β : Type u_2} [Semigroup α] [Semigroup β] {F : Type u_3} [EquivLike F α β] [MulEquivClass F α β] (f : F) [DecompositionMonoid β] :
DecompositionMonoid α
source
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 := ⋯ }
Instances For
    source
    @[simp]
    theorem Equiv.dvd_apply {G : Type u_4} [LeftCancelSemigroup G] (g a : G) :
    ↑((Equiv.dvd g) a) = g * a
    source
    theorem dvd_add {α : Type u_1} [Add α] [Semigroup α] [LeftDistribClass α] {a b c : α} (h₁ : a ∣ b) (h₂ : a ∣ c) :
    a ∣ b + c
    source
    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.

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

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

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

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

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

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

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

    Alias of dvd_sub.

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

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

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

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

    source
    theorem dvd_iff_dvd_of_dvd_sub {α : Type u_1} [NonUnitalRing α] {a b c : α} (h : a ∣ b - c) :
    a ∣ b ↔ a ∣ c
    source
    theorem dvd_sub_comm {α : Type u_1} [NonUnitalRing α] {a b c : α} :
    a ∣ b - c ↔ a ∣ c - b
    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} [NonUnitalCommRing α] {k a b x y : α} (hab : k ∣ a - b) (hxy : k ∣ x - y) :
    k ∣ a * x - b * y