Mathlib.Algebra.Ring.Divisibility.Basic

map_dvd_iff theorem

(f : F) {a b} : f a ∣ f b ↔ a ∣ b

Full source

theorem map_dvd_iff (f : F) {a b} : f a ∣ f bf a ∣ f b ↔ a ∣ b :=
  let f := MulEquivClass.toMulEquiv f
  ⟨fun h ↦ by rw [← f.left_inv a, ← f.left_inv b]; exact map_dvd f.symm h, map_dvd f⟩

Divisibility Preservation Under Multiplicative Equivalence: $f(a) \mid f(b) \leftrightarrow a \mid b$

Informal description

Let $M$ and $N$ be semigroups, and let $F$ be a type of multiplicative equivalences between $M$ and $N$. For any multiplicative equivalence $f \colon M \to N$ in $F$ and any elements $a, b \in M$, the element $f(a)$ divides $f(b)$ in $N$ if and only if $a$ divides $b$ in $M$.

MulEquiv.decompositionMonoid theorem

(f : F) [DecompositionMonoid β] : DecompositionMonoid α

Full source

theorem MulEquiv.decompositionMonoid (f : F) [DecompositionMonoid β] : DecompositionMonoid α where
  primal a b c h := by
    rw [← map_dvd_iff f, map_mul] at h
    obtain ⟨a₁, a₂, h⟩ := DecompositionMonoid.primal _ h
    refine ⟨symm f a₁, symm f a₂, ?_⟩
    simp_rw [← map_dvd_iff f, ← map_mul, eq_symm_apply]
    iterate 2 erw [(f : α ≃* β).apply_symm_apply]
    exact h

Decomposition Monoid Property Preserved Under Multiplicative Equivalence

Informal description

Let $\alpha$ and $\beta$ be semigroups, and let $F$ be a type of multiplicative equivalences between $\alpha$ and $\beta$. Given a multiplicative equivalence $f \colon \alpha \to \beta$ in $F$ and assuming $\beta$ is a decomposition monoid, then $\alpha$ is also a decomposition monoid.

Equiv.dvd definition

{G : Type*} [LeftCancelSemigroup G] (g : G) : G ≃ { a : G // g ∣ a }

Full source

/--
If `G` is a `LeftCancelSemiGroup`, left multiplication by `g` yields an equivalence between `G`
and the set of elements of `G` divisible by `g`.
-/
protected noncomputable def Equiv.dvd {G : Type*} [LeftCancelSemigroup G] (g : G) :
    G ≃ {a : G // g ∣ a} where
  toFun := fun a ↦ ⟨g * a, ⟨a, rfl⟩⟩
  invFun := fun ⟨_, h⟩ ↦ h.choose
  left_inv := fun _ ↦ by simp
  right_inv := by
    rintro ⟨_, ⟨_, rfl⟩⟩
    simp

Bijection between elements and their multiples in a left cancellative semigroup

Informal description

For a left cancellative semigroup $G$ and an element $g \in G$, the function $a \mapsto g * a$ defines a bijection between $G$ and the set of elements in $G$ divisible by $g$. More precisely, the equivalence $\text{Equiv.dvd}\, g : G \simeq \{ a \in G \mid g \mid a \}$ is given by: - The forward map sends $a \in G$ to $g * a$ (which is divisible by $g$ by definition). - The inverse map sends an element $\langle a, h \rangle$ in $\{ a \in G \mid g \mid a \}$ to the unique $b \in G$ such that $a = g * b$ (which exists and is unique by left cancellation and the divisibility condition $g \mid a$).

Equiv.dvd_apply theorem

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

Full source

@[simp]
theorem Equiv.dvd_apply {G : Type*} [LeftCancelSemigroup G] (g a : G) :
    Equiv.dvd g a = g * a := rfl

Forward Map of Divisibility Bijection in Left Cancellative Semigroup

Informal description

For any left cancellative semigroup $G$ and elements $g, a \in G$, the forward map of the bijection $\text{Equiv.dvd}\, g$ evaluated at $a$ is equal to $g * a$.

dvd_add theorem

[LeftDistribClass α] {a b c : α} (h₁ : a ∣ b) (h₂ : a ∣ c) : a ∣ b + c

Full source

theorem dvd_add [LeftDistribClass α] {a b c : α} (h₁ : a ∣ b) (h₂ : a ∣ c) : a ∣ b + c :=
  Dvd.elim h₁ fun d hd => Dvd.elim h₂ fun e he => Dvd.intro (d + e) (by simp [left_distrib, hd, he])

Divisibility of Sum: $a \mid b$ and $a \mid c$ implies $a \mid (b + c)$

Informal description

Let $\alpha$ be a type with addition and multiplication operations satisfying left distributivity. For any elements $a, b, c \in \alpha$, if $a$ divides $b$ and $a$ divides $c$, then $a$ divides their sum $b + c$.

min_pow_dvd_add theorem

(ha : c ^ m ∣ a) (hb : c ^ n ∣ b) : c ^ min m n ∣ a + b

Full source

lemma min_pow_dvd_add (ha : c ^ m ∣ a) (hb : c ^ n ∣ b) : c ^ min m n ∣ a + b :=
  ((pow_dvd_pow c (m.min_le_left n)).trans ha).add ((pow_dvd_pow c (m.min_le_right n)).trans hb)

Minimum Power Divisibility of Sum: $c^{\min(m,n)} \mid (a + b)$ when $c^m \mid a$ and $c^n \mid b$

Informal description

Let $\alpha$ be a semiring and let $a, b, c \in \alpha$ and $m, n \in \mathbb{N}$. If $c^m$ divides $a$ and $c^n$ divides $b$, then $c^{\min(m,n)}$ divides $a + b$.

Dvd.dvd.linear_comb theorem

{d x y : α} (hdx : d ∣ x) (hdy : d ∣ y) (a b : α) : d ∣ a * x + b * y

Full source

theorem Dvd.dvd.linear_comb {d x y : α} (hdx : d ∣ x) (hdy : d ∣ y) (a b : α) : d ∣ a * x + b * y :=
  dvd_add (hdx.mul_left a) (hdy.mul_left b)

Divisibility of Linear Combinations: $d \mid (a \cdot x + b \cdot y)$ when $d \mid x$ and $d \mid y$

Informal description

Let $\alpha$ be a semiring and let $d, x, y \in \alpha$. If $d$ divides $x$ and $d$ divides $y$, then for any $a, b \in \alpha$, $d$ divides the linear combination $a \cdot x + b \cdot y$.

dvd_neg theorem

: a ∣ -b ↔ a ∣ b

Full source

/-- An element `a` of a semigroup with a distributive negation divides the negation of an element
`b` iff `a` divides `b`. -/
@[simp]
theorem dvd_neg : a ∣ -ba ∣ -b ↔ a ∣ b :=
  (Equiv.neg _).exists_congr_left.trans <| by
    simp only [Equiv.neg_symm, Equiv.neg_apply, mul_neg, neg_inj, Dvd.dvd]

Divisibility of Negated Element: $a \mid -b \leftrightarrow a \mid b$

Informal description

For any elements $a$ and $b$ in a semigroup with distributive negation, $a$ divides $-b$ if and only if $a$ divides $b$.

neg_dvd theorem

: -a ∣ b ↔ a ∣ b

Full source

/-- The negation of an element `a` of a semigroup with a distributive negation divides another
element `b` iff `a` divides `b`. -/
@[simp]
theorem neg_dvd : -a ∣ b-a ∣ b ↔ a ∣ b :=
  (Equiv.neg _).exists_congr_left.trans <| by
    simp only [Equiv.neg_symm, Equiv.neg_apply, mul_neg, neg_mul, neg_neg, Dvd.dvd]

Negation Preserves Divisibility: $-a \mid b \leftrightarrow a \mid b$

Informal description

For any elements $a$ and $b$ in a semigroup with distributive negation, $-a$ divides $b$ if and only if $a$ divides $b$.

dvd_sub theorem

(h₁ : a ∣ b) (h₂ : a ∣ c) : a ∣ b - c

Full source

theorem dvd_sub (h₁ : a ∣ b) (h₂ : a ∣ c) : a ∣ b - c := by
  simpa only [← sub_eq_add_neg] using h₁.add h₂.neg_right

Divisibility of Difference: $a \mid b$ and $a \mid c$ implies $a \mid (b - c)$

Informal description

For any elements $a$, $b$, and $c$ in a non-unital ring, if $a$ divides $b$ and $a$ divides $c$, then $a$ divides $b - c$.

dvd_add_left theorem

(h : a ∣ c) : a ∣ b + c ↔ a ∣ b

Full source

/-- 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_left (h : a ∣ c) : a ∣ b + ca ∣ b + c ↔ a ∣ b :=
  ⟨fun H => by simpa only [add_sub_cancel_right] using dvd_sub H h, fun h₂ => dvd_add h₂ h⟩

Divisibility of Sum: $a \mid c$ implies $a \mid (b + c) \leftrightarrow a \mid b$

Informal description

Let $a$, $b$, and $c$ be elements in a ring. If $a$ divides $c$, then $a$ divides $b + c$ if and only if $a$ divides $b$.

dvd_add_right theorem

(h : a ∣ b) : a ∣ b + c ↔ a ∣ c

Full source

/-- 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_add_right (h : a ∣ b) : a ∣ b + ca ∣ b + c ↔ a ∣ c := by rw [add_comm]; exact dvd_add_left h

Divisibility of Sum: $a \mid b$ implies $a \mid (b + c) \leftrightarrow a \mid c$

Informal description

Let $a$, $b$, and $c$ be elements in a ring. If $a$ divides $b$, then $a$ divides $b + c$ if and only if $a$ divides $c$.

dvd_sub_left theorem

(h : a ∣ c) : a ∣ b - c ↔ a ∣ b

Full source

/-- 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_left (h : a ∣ c) : a ∣ b - ca ∣ b - c ↔ a ∣ b := by
  simpa only [← sub_eq_add_neg] using dvd_add_left (dvd_neg.2 h)

Divisibility of Difference: $a \mid c$ implies $a \mid (b - c) \leftrightarrow a \mid b$

Informal description

Let $a$, $b$, and $c$ be elements in a ring. If $a$ divides $c$, then $a$ divides $b - c$ if and only if $a$ divides $b$.

dvd_sub_right theorem

(h : a ∣ b) : a ∣ b - c ↔ a ∣ c

Full source

/-- 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_sub_right (h : a ∣ b) : a ∣ b - ca ∣ b - c ↔ a ∣ c := by
  rw [sub_eq_add_neg, dvd_add_right h, dvd_neg]

Divisibility of Difference: $a \mid b$ implies $a \mid (b - c) \leftrightarrow a \mid c$

Informal description

Let $a$, $b$, and $c$ be elements in a ring. If $a$ divides $b$, then $a$ divides $b - c$ if and only if $a$ divides $c$.

dvd_iff_dvd_of_dvd_sub theorem

(h : a ∣ b - c) : a ∣ b ↔ a ∣ c

Full source

theorem dvd_iff_dvd_of_dvd_sub (h : a ∣ b - c) : a ∣ ba ∣ b ↔ a ∣ c := by
  rw [← sub_add_cancel b c, dvd_add_right h]

Divisibility Criterion via Difference: $a \mid (b - c)$ implies $a \mid b \leftrightarrow a \mid c$

Informal description

Let $a$, $b$, and $c$ be elements in a ring. If $a$ divides $b - c$, then $a$ divides $b$ if and only if $a$ divides $c$.

dvd_sub_comm theorem

: a ∣ b - c ↔ a ∣ c - b

Full source

theorem dvd_sub_comm : a ∣ b - ca ∣ b - c ↔ a ∣ c - b := by rw [← dvd_neg, neg_sub]

Divisibility of Difference is Commutative: $a \mid (b - c) \leftrightarrow a \mid (c - b)$

Informal description

For any elements $a$, $b$, and $c$ in a non-unital non-associative ring with distributive negation, $a$ divides $b - c$ if and only if $a$ divides $c - b$.

dvd_add_self_left theorem

{a b : α} : a ∣ a + b ↔ a ∣ b

Full source

/-- An element a divides the sum a + b if and only if a divides b. -/
@[simp]
theorem dvd_add_self_left {a b : α} : a ∣ a + ba ∣ a + b ↔ a ∣ b :=
  dvd_add_right (dvd_refl a)

Divisibility of Sum with Self on Left: $a \mid (a + b) \leftrightarrow a \mid b$

Informal description

For any elements $a$ and $b$ in a ring, $a$ divides $a + b$ if and only if $a$ divides $b$.

dvd_add_self_right theorem

{a b : α} : a ∣ b + a ↔ a ∣ b

Full source

/-- An element a divides the sum b + a if and only if a divides b. -/
@[simp]
theorem dvd_add_self_right {a b : α} : a ∣ b + aa ∣ b + a ↔ a ∣ b :=
  dvd_add_left (dvd_refl a)

Divisibility of Sum with Self on Right: $a \mid (b + a) \leftrightarrow a \mid b$

Informal description

For any elements $a$ and $b$ in a ring, $a$ divides $b + a$ if and only if $a$ divides $b$.

dvd_sub_self_left theorem

: a ∣ a - b ↔ a ∣ b

Full source

/-- An element `a` divides the difference `a - b` if and only if `a` divides `b`. -/
@[simp]
theorem dvd_sub_self_left : a ∣ a - ba ∣ a - b ↔ a ∣ b :=
  dvd_sub_right dvd_rfl

Divisibility of Difference with Self on Left: $a \mid (a - b) \leftrightarrow a \mid b$

Informal description

For any elements $a$ and $b$ in a ring, $a$ divides $a - b$ if and only if $a$ divides $b$.

dvd_sub_self_right theorem

: a ∣ b - a ↔ a ∣ b

Full source

/-- An element `a` divides the difference `b - a` if and only if `a` divides `b`. -/
@[simp]
theorem dvd_sub_self_right : a ∣ b - aa ∣ b - a ↔ a ∣ b :=
  dvd_sub_left dvd_rfl

Divisibility of Difference with Self on Right: $a \mid (b - a) \leftrightarrow a \mid b$

Informal description

For any elements $a$ and $b$ in a ring, $a$ divides $b - a$ if and only if $a$ divides $b$.

dvd_mul_sub_mul theorem

{k a b x y : α} (hab : k ∣ a - b) (hxy : k ∣ x - y) : k ∣ a * x - b * y

Full source

theorem dvd_mul_sub_mul {k a b x y : α} (hab : k ∣ a - b) (hxy : k ∣ x - y) :
    k ∣ a * x - b * y := by
  convert dvd_add (hxy.mul_left a) (hab.mul_right y) using 1
  rw [mul_sub_left_distrib, mul_sub_right_distrib]
  simp only [sub_eq_add_neg, add_assoc, neg_add_cancel_left]

Divisibility of Product Differences: $k \mid (a - b)$ and $k \mid (x - y)$ implies $k \mid (a x - b y)$

Informal description

Let $\alpha$ be a non-unital commutative ring. For any elements $k, a, b, x, y \in \alpha$, if $k$ divides $a - b$ and $k$ divides $x - y$, then $k$ divides $a \cdot x - b \cdot y$.