doc-next-gen

Mathlib.Algebra.Divisibility.Basic

Module docstring

{"# Divisibility

This file defines the basics of the divisibility relation in the context of (Comm) Monoids.

Main definitions

  • semigroupDvd

Implementation notes

The divisibility relation is defined for all monoids, and as such, depends on the order of multiplication if the monoid is not commutative. There are two possible conventions for divisibility in the noncommutative context, and this relation follows the convention for ordinals, so a | b is defined as ∃ c, b = a * c.

Tags

divisibility, divides "}

semigroupDvd instance
: Dvd α
Full source 
/-- There are two possible conventions for divisibility, which coincide in a `CommMonoid`.
    This matches the convention for ordinals. -/
instance (priority := 100) semigroupDvd : Dvd α :=
  Dvd.mk fun a b => ∃ c, b = a * c
Divisibility Relation in Semigroups
Informal description
For any semigroup $\alpha$, the divisibility relation $a \mid b$ is defined by the existence of an element $c$ such that $b = a * c$.
Dvd.intro theorem
(c : α) (h : a * c = b) : a ∣ b
Full source 
theorem Dvd.intro (c : α) (h : a * c = b) : a ∣ b :=
  Exists.intro c h.symm
Divisibility Introduction: $b = a \cdot c$ implies $a \mid b$
Informal description
For any elements $a$, $b$, and $c$ in a semigroup $\alpha$, if $b = a \cdot c$, then $a$ divides $b$ (denoted $a \mid b$).
exists_eq_mul_right_of_dvd theorem
(h : a ∣ b) : ∃ c, b = a * c
Full source 
theorem exists_eq_mul_right_of_dvd (h : a ∣ b) : ∃ c, b = a * c :=
  h
Existence of Right Factor in Divisibility
Informal description
For any elements $a$ and $b$ in a semigroup, if $a$ divides $b$ (denoted $a \mid b$), then there exists an element $c$ such that $b = a \cdot c$.
dvd_def theorem
: a ∣ b ↔ ∃ c, b = a * c
Full source 
theorem dvd_def : a ∣ ba ∣ b ↔ ∃ c, b = a * c :=
  Iff.rfl
Definition of Divisibility in Semigroups: $a \mid b \leftrightarrow \exists c, b = a \cdot c$
Informal description
For any elements $a$ and $b$ in a semigroup, $a$ divides $b$ (denoted $a \mid b$) if and only if there exists an element $c$ such that $b = a \cdot c$.
Dvd.elim theorem
{P : Prop} {a b : α} (H₁ : a ∣ b) (H₂ : ∀ c, b = a * c → P) : P
Full source 
theorem Dvd.elim {P : Prop} {a b : α} (H₁ : a ∣ b) (H₂ : ∀ c, b = a * c → P) : P :=
  Exists.elim H₁ H₂
Elimination Principle for Divisibility in Semigroups
Informal description
For any elements $a$ and $b$ in a semigroup, if $a$ divides $b$ (i.e., there exists $c$ such that $b = a \cdot c$), and if for every $c$ satisfying $b = a \cdot c$ we can prove a proposition $P$, then $P$ holds.
dvd_trans theorem
: a ∣ b → b ∣ c → a ∣ c
Full source 
@[trans]
theorem dvd_trans : a ∣ b → b ∣ c → a ∣ c
  | ⟨d, h₁⟩, ⟨e, h₂⟩ => ⟨d * e, h₁ ▸ h₂.trans <| mul_assoc a d e⟩
Transitivity of Divisibility in Semigroups
Informal description
For any elements $a$, $b$, and $c$ in a semigroup, if $a$ divides $b$ and $b$ divides $c$, then $a$ divides $c$.
instIsTransDvd instance
: IsTrans α Dvd.dvd
Full source 
/-- Transitivity of `|` for use in `calc` blocks. -/
instance : IsTrans α Dvd.dvd :=
  ⟨fun _ _ _ => dvd_trans⟩
Transitivity of Divisibility in Semigroups
Informal description
The divisibility relation $\mid$ on a semigroup $\alpha$ is transitive.
dvd_mul_right theorem
(a b : α) : a ∣ a * b
Full source 
@[simp]
theorem dvd_mul_right (a b : α) : a ∣ a * b :=
  Dvd.intro b rfl
Divisibility of Right Multiple: $a \mid a \cdot b$
Informal description
For any elements $a$ and $b$ in a semigroup, $a$ divides the product $a \cdot b$.
dvd_mul_of_dvd_left theorem
(h : a ∣ b) (c : α) : a ∣ b * c
Full source 
theorem dvd_mul_of_dvd_left (h : a ∣ b) (c : α) : a ∣ b * c :=
  h.trans (dvd_mul_right b c)
Divisibility of Product by Left Divisor: $a \mid b \Rightarrow a \mid b \cdot c$
Informal description
For any elements $a, b, c$ in a semigroup, if $a$ divides $b$, then $a$ divides the product $b \cdot c$.
dvd_of_mul_right_dvd theorem
(h : a * b ∣ c) : a ∣ c
Full source 
theorem dvd_of_mul_right_dvd (h : a * b ∣ c) : a ∣ c :=
  (dvd_mul_right a b).trans h
Divisibility from Right Multiple: $a \cdot b \mid c \Rightarrow a \mid c$
Informal description
For any elements $a$, $b$, and $c$ in a semigroup, if the product $a \cdot b$ divides $c$, then $a$ divides $c$.
IsPrimal definition
(a : α) : Prop
Full source 
/-- An element `a` in a semigroup is primal if whenever `a` is a divisor of `b * c`, it can be
factored as the product of a divisor of `b` and a divisor of `c`. -/
def IsPrimal (a : α) : Prop := ∀ ⦃b c⦄, a ∣ b * c → ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂
Primal element in a semigroup
Informal description
An element $a$ in a semigroup $\alpha$ is called *primal* if for any elements $b, c \in \alpha$ such that $a$ divides $b \cdot c$, there exist elements $a_1, a_2 \in \alpha$ such that $a_1$ divides $b$, $a_2$ divides $c$, and $a = a_1 \cdot a_2$.
DecompositionMonoid structure
Full source 
/-- A monoid is a decomposition monoid if every element is primal. An integral domain whose
multiplicative monoid is a decomposition monoid, is called a pre-Schreier domain; it is a
Schreier domain if it is moreover integrally closed. -/
@[mk_iff] class DecompositionMonoid : Prop where
  primal (a : α) : IsPrimal a
Decomposition Monoid
Informal description
A decomposition monoid is a monoid in which every element is primal, meaning that for any element $a$ dividing a product $b \cdot c$, there exist elements $a_1$ and $a_2$ such that $a_1$ divides $b$, $a_2$ divides $c$, and $a = a_1 \cdot a_2$.
exists_dvd_and_dvd_of_dvd_mul theorem
[DecompositionMonoid α] {b c a : α} (H : a ∣ b * c) : ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂
Full source 
theorem exists_dvd_and_dvd_of_dvd_mul [DecompositionMonoid α] {b c a : α} (H : a ∣ b * c) :
    ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂ := DecompositionMonoid.primal a H
Decomposition of Divisors in a Decomposition Monoid
Informal description
Let $\alpha$ be a decomposition monoid. For any elements $a, b, c \in \alpha$ such that $a$ divides $b \cdot c$, there exist elements $a_1, a_2 \in \alpha$ such that $a_1$ divides $b$, $a_2$ divides $c$, and $a = a_1 \cdot a_2$.
dvd_refl theorem
(a : α) : a ∣ a
Full source 
@[refl, simp]
theorem dvd_refl (a : α) : a ∣ a :=
  Dvd.intro 1 (mul_one a)
Reflexivity of Divisibility: $a \mid a$
Informal description
For any element $a$ in a semigroup $\alpha$, $a$ divides itself, i.e., $a \mid a$.
dvd_rfl theorem
: ∀ {a : α}, a ∣ a
Full source 
theorem dvd_rfl : ∀ {a : α}, a ∣ a := fun {a} => dvd_refl a
Reflexivity of Divisibility: $a \mid a$
Informal description
For any element $a$ in a semigroup $\alpha$, $a$ divides itself, i.e., $a \mid a$.
instIsReflDvd instance
: IsRefl α (· ∣ ·)
Full source 
instance : IsRefl α (· ∣ ·) :=
  ⟨dvd_refl⟩
Reflexivity of Divisibility in Semigroups
Informal description
For any semigroup $\alpha$, the divisibility relation $\mid$ is reflexive.
one_dvd theorem
(a : α) : 1 ∣ a
Full source 
theorem one_dvd (a : α) : 1 ∣ a :=
  Dvd.intro a (one_mul a)
Divisibility by One in a Monoid
Informal description
For any element $a$ in a monoid $\alpha$, the multiplicative identity $1$ divides $a$, i.e., $1 \mid a$.
dvd_of_eq theorem
(h : a = b) : a ∣ b
Full source 
theorem dvd_of_eq (h : a = b) : a ∣ b := by rw [h]
Divisibility from Equality: $a = b \Rightarrow a \mid b$
Informal description
For any elements $a$ and $b$ in a semigroup $\alpha$, if $a = b$, then $a$ divides $b$, i.e., $a \mid b$.
dvd_pow theorem
(hab : a ∣ b) : ∀ {n : ℕ} (_ : n ≠ 0), a ∣ b ^ n
Full source 
lemma dvd_pow (hab : a ∣ b) : ∀ {n : ℕ} (_ : n ≠ 0), a ∣ b ^ n
  | 0,     hn => (hn rfl).elim
  | n + 1, _  => by rw [pow_succ']; exact hab.mul_right _
Divisibility of Powers: $a \mid b \Rightarrow a \mid b^n$ for $n \neq 0$
Informal description
For any elements $a$ and $b$ in a monoid $\alpha$, if $a$ divides $b$, then for any nonzero natural number $n$, $a$ divides $b^n$.
dvd_pow_self theorem
(a : α) {n : ℕ} (hn : n ≠ 0) : a ∣ a ^ n
Full source 
lemma dvd_pow_self (a : α) {n : ℕ} (hn : n ≠ 0) : a ∣ a ^ n := dvd_rfl.pow hn
Self-Divisibility of Powers: $a \mid a^n$ for $n \neq 0$
Informal description
For any element $a$ in a monoid $\alpha$ and any nonzero natural number $n$, $a$ divides $a^n$.
mul_dvd_mul_left theorem
(a : α) (h : b ∣ c) : a * b ∣ a * c
Full source 
theorem mul_dvd_mul_left (a : α) (h : b ∣ c) : a * b ∣ a * c := by
  obtain ⟨d, rfl⟩ := h
  use d
  rw [mul_assoc]
Left Multiplication Preserves Divisibility in Semigroups
Informal description
For any elements $a, b, c$ in a semigroup $\alpha$, if $b$ divides $c$, then the product $a * b$ divides $a * c$.
Dvd.intro_left theorem
(c : α) (h : c * a = b) : a ∣ b
Full source 
theorem Dvd.intro_left (c : α) (h : c * a = b) : a ∣ b :=
  Dvd.intro c (by rw [mul_comm] at h; apply h)
Divisibility from Left Factor: $b = c \cdot a$ implies $a \mid b$
Informal description
For any elements $a$, $b$, and $c$ in a semigroup $\alpha$, if $b = c \cdot a$, then $a$ divides $b$ (denoted $a \mid b$).
exists_eq_mul_left_of_dvd theorem
(h : a ∣ b) : ∃ c, b = c * a
Full source 
theorem exists_eq_mul_left_of_dvd (h : a ∣ b) : ∃ c, b = c * a :=
  Dvd.elim h fun c => fun H1 : b = a * c => Exists.intro c (Eq.trans H1 (mul_comm a c))
Existence of Left Factor in Divisibility Relation
Informal description
For any elements $a$ and $b$ in a semigroup, if $a$ divides $b$, then there exists an element $c$ such that $b = c * a$.
Dvd.elim_left theorem
{P : Prop} (h₁ : a ∣ b) (h₂ : ∀ c, b = c * a → P) : P
Full source 
theorem Dvd.elim_left {P : Prop} (h₁ : a ∣ b) (h₂ : ∀ c, b = c * a → P) : P :=
  Exists.elim (exists_eq_mul_left_of_dvd h₁) fun c => fun h₃ : b = c * a => h₂ c h₃
Elimination Principle for Left Divisibility in Semigroups
Informal description
For any elements $a$ and $b$ in a semigroup, if $a$ divides $b$, then to prove a proposition $P$, it suffices to show that for all elements $c$ such that $b = c * a$, the proposition $P$ holds.
dvd_mul_left theorem
(a b : α) : a ∣ b * a
Full source 
@[simp]
theorem dvd_mul_left (a b : α) : a ∣ b * a :=
  Dvd.intro b (mul_comm a b)
Left Divisibility in Semigroups: $a \mid b \cdot a$
Informal description
For any elements $a$ and $b$ in a semigroup $\alpha$, the element $a$ divides the product $b * a$.
dvd_mul_of_dvd_right theorem
(h : a ∣ b) (c : α) : a ∣ c * b
Full source 
theorem dvd_mul_of_dvd_right (h : a ∣ b) (c : α) : a ∣ c * b := by
  rw [mul_comm]; exact h.mul_right _
Divisibility of Right Multiple: $a \mid b \implies a \mid c \cdot b$
Informal description
For any elements $a$ and $b$ in a semigroup $\alpha$, if $a$ divides $b$, then for any element $c \in \alpha$, $a$ divides the product $c \cdot b$.
mul_dvd_mul theorem
: ∀ {a b c d : α}, a ∣ b → c ∣ d → a * c ∣ b * d
Full source 
theorem mul_dvd_mul : ∀ {a b c d : α}, a ∣ b → c ∣ d → a * c ∣ b * d
  | a, _, c, _, ⟨e, rfl⟩, ⟨f, rfl⟩ => ⟨e * f, by simp⟩
Product Divisibility: $a \mid b \land c \mid d \implies a \cdot c \mid b \cdot d$
Informal description
For any elements $a, b, c, d$ in a semigroup $\alpha$, if $a$ divides $b$ and $c$ divides $d$, then the product $a \cdot c$ divides the product $b \cdot d$.
dvd_of_mul_left_dvd theorem
(h : a * b ∣ c) : b ∣ c
Full source 
theorem dvd_of_mul_left_dvd (h : a * b ∣ c) : b ∣ c :=
  Dvd.elim h fun d ceq => Dvd.intro (a * d) (by simp [ceq])
Divisibility by Right Factor: $a \cdot b \mid c$ implies $b \mid c$
Informal description
For any elements $a, b, c$ in a semigroup, if $a \cdot b$ divides $c$, then $b$ divides $c$.
dvd_mul theorem
[DecompositionMonoid α] {k m n : α} : k ∣ m * n ↔ ∃ d₁ d₂, d₁ ∣ m ∧ d₂ ∣ n ∧ k = d₁ * d₂
Full source 
theorem dvd_mul [DecompositionMonoid α] {k m n : α} :
    k ∣ m * nk ∣ m * n ↔ ∃ d₁ d₂, d₁ ∣ m ∧ d₂ ∣ n ∧ k = d₁ * d₂ := by
  refine ⟨exists_dvd_and_dvd_of_dvd_mul, ?_⟩
  rintro ⟨d₁, d₂, hy, hz, rfl⟩
  exact mul_dvd_mul hy hz
Divisibility of Product in Decomposition Monoid: $k \mid m \cdot n \leftrightarrow \exists d_1, d_2, (d_1 \mid m) \land (d_2 \mid n) \land (k = d_1 \cdot d_2)$
Informal description
Let $\alpha$ be a decomposition monoid. For any elements $k, m, n \in \alpha$, the element $k$ divides the product $m \cdot n$ if and only if there exist elements $d_1, d_2 \in \alpha$ such that $d_1$ divides $m$, $d_2$ divides $n$, and $k = d_1 \cdot d_2$.
mul_dvd_mul_right theorem
(h : a ∣ b) (c : α) : a * c ∣ b * c
Full source 
theorem mul_dvd_mul_right (h : a ∣ b) (c : α) : a * c ∣ b * c :=
  mul_dvd_mul h (dvd_refl c)
Right Multiplication Preserves Divisibility: $a \mid b \implies a \cdot c \mid b \cdot c$
Informal description
For any elements $a, b, c$ in a semigroup $\alpha$, if $a$ divides $b$, then the product $a \cdot c$ divides the product $b \cdot c$.
pow_dvd_pow_of_dvd theorem
(h : a ∣ b) : ∀ n : ℕ, a ^ n ∣ b ^ n
Full source 
theorem pow_dvd_pow_of_dvd (h : a ∣ b) : ∀ n : ℕ, a ^ n ∣ b ^ n
  | 0 => by rw [pow_zero, pow_zero]
  | n + 1 => by
    rw [pow_succ, pow_succ]
    exact mul_dvd_mul (pow_dvd_pow_of_dvd h n) h
Power Divisibility: $a \mid b \implies a^n \mid b^n$
Informal description
For any elements $a$ and $b$ in a monoid, if $a$ divides $b$, then for any natural number $n$, the $n$-th power of $a$ divides the $n$-th power of $b$, i.e., $a^n \mid b^n$.