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

instance semigroupDvd {α : Type u_1} [Semigroup α] : Dvd α

There are two possible conventions for divisibility, which coincide in a CommMonoid. This matches the convention for ordinals.

Equations

• semigroupDvd = { dvd := fun (a b : α) => ∃ (c : α), b = a * c }

theorem Dvd.intro {α : Type u_1} [Semigroup α] {a : α} {b : α} (c : α) (h : a * c = b) : a ∣ b

theorem dvd_of_mul_right_eq {α : Type u_1} [Semigroup α] {a : α} {b : α} (c : α) (h : a * c = b) : a ∣ b

Alias of Dvd.intro.

theorem exists_eq_mul_right_of_dvd {α : Type u_1} [Semigroup α] {a : α} {b : α} (h : a ∣ b) : ∃ (c : α), b = a * c

theorem dvd_def {α : Type u_1} [Semigroup α] {a : α} {b : α} : a ∣ b ↔ ∃ (c : α), b = a * c

theorem dvd_iff_exists_eq_mul_right {α : Type u_1} [Semigroup α] {a : α} {b : α} : a ∣ b ↔ ∃ (c : α), b = a * c

Alias of dvd_def.

theorem Dvd.elim {α : Type u_1} [Semigroup α] {P : Prop} {a : α} {b : α} (H₁ : a ∣ b) (H₂ : ∀ (c : α), b = a * c → P) : P

theorem dvd_trans {α : Type u_1} [Semigroup α] {a : α} {b : α} {c : α} : a ∣ b → b ∣ c → a ∣ c

theorem Dvd.dvd.trans {α : Type u_1} [Semigroup α] {a : α} {b : α} {c : α} : a ∣ b → b ∣ c → a ∣ c

Alias of dvd_trans.

instance instIsTransDvdSemigroupDvd {α : Type u_1} [Semigroup α] : IsTrans α Dvd.dvd

Transitivity of | for use in calc blocks.

Equations

• ⋯ = ⋯

@[simp]

theorem dvd_mul_right {α : Type u_1} [Semigroup α] (a : α) (b : α) : a ∣ a * b

theorem dvd_mul_of_dvd_left {α : Type u_1} [Semigroup α] {a : α} {b : α} (h : a ∣ b) (c : α) : a ∣ b * c

theorem Dvd.dvd.mul_right {α : Type u_1} [Semigroup α] {a : α} {b : α} (h : a ∣ b) (c : α) : a ∣ b * c

Alias of dvd_mul_of_dvd_left.

theorem dvd_of_mul_right_dvd {α : Type u_1} [Semigroup α] {a : α} {b : α} {c : α} (h : a * b ∣ c) : a ∣ c

theorem map_dvd {M : Type u_2} {N : Type u_3} [Semigroup M] [Semigroup N] {F : Type u_4} [FunLike F M N] [MulHomClass F M N] (f : F) {a : M} {b : M} : a ∣ b → f a ∣ f b

theorem MulHom.map_dvd {M : Type u_2} {N : Type u_3} [Semigroup M] [Semigroup N] (f : M →ₙ* N) {a : M} {b : M} : a ∣ b → f a ∣ f b

theorem MonoidHom.map_dvd {M : Type u_2} {N : Type u_3} [Monoid M] [Monoid N] (f : M →* N) {a : M} {b : M} : a ∣ b → f a ∣ f b

def IsPrimal {α : Type u_1} [Semigroup α] (a : α) : Prop

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.

Equations

• IsPrimal a = ∀ ⦃b c : α⦄, a ∣ b * c → ∃ (a₁ : α), ∃ (a₂ : α), a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂

theorem decompositionMonoid_iff (α : Type u_1) [Semigroup α] : DecompositionMonoid α ↔ ∀ (a : α), IsPrimal a

class DecompositionMonoid (α : Type u_1) [Semigroup α] : Prop

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.

• primal : ∀ (a : α), IsPrimal a

theorem exists_dvd_and_dvd_of_dvd_mul {α : Type u_1} [Semigroup α] [DecompositionMonoid α] {b : α} {c : α} {a : α} (H : a ∣ b * c) : ∃ (a₁ : α), ∃ (a₂ : α), a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂

@[simp]

theorem dvd_refl {α : Type u_1} [Monoid α] (a : α) : a ∣ a

theorem dvd_rfl {α : Type u_1} [Monoid α] {a : α} : a ∣ a

instance instIsReflDvdSemigroupDvdToSemigroup {α : Type u_1} [Monoid α] : IsRefl α fun (x x_1 : α) => x ∣ x_1

Equations

• ⋯ = ⋯

theorem one_dvd {α : Type u_1} [Monoid α] (a : α) : 1 ∣ a

theorem dvd_of_eq {α : Type u_1} [Monoid α] {a : α} {b : α} (h : a = b) : a ∣ b

theorem Eq.dvd {α : Type u_1} [Monoid α] {a : α} {b : α} (h : a = b) : a ∣ b

Alias of dvd_of_eq.

theorem pow_dvd_pow {α : Type u_1} [Monoid α] {m : ℕ} {n : ℕ} (a : α) (h : m ≤ n) : a ^ m ∣ a ^ n

theorem dvd_pow {α : Type u_1} [Monoid α] {a : α} {b : α} (hab : a ∣ b) {n : ℕ} : n ≠ 0 → a ∣ b ^ n

theorem Dvd.dvd.pow {α : Type u_1} [Monoid α] {a : α} {b : α} (hab : a ∣ b) {n : ℕ} : n ≠ 0 → a ∣ b ^ n

Alias of dvd_pow.

theorem dvd_pow_self {α : Type u_1} [Monoid α] (a : α) {n : ℕ} (hn : n ≠ 0) : a ∣ a ^ n

theorem Dvd.intro_left {α : Type u_1} [CommSemigroup α] {a : α} {b : α} (c : α) (h : c * a = b) : a ∣ b

theorem dvd_of_mul_left_eq {α : Type u_1} [CommSemigroup α] {a : α} {b : α} (c : α) (h : c * a = b) : a ∣ b

Alias of Dvd.intro_left.

theorem exists_eq_mul_left_of_dvd {α : Type u_1} [CommSemigroup α] {a : α} {b : α} (h : a ∣ b) : ∃ (c : α), b = c * a

theorem dvd_iff_exists_eq_mul_left {α : Type u_1} [CommSemigroup α] {a : α} {b : α} : a ∣ b ↔ ∃ (c : α), b = c * a

theorem Dvd.elim_left {α : Type u_1} [CommSemigroup α] {a : α} {b : α} {P : Prop} (h₁ : a ∣ b) (h₂ : ∀ (c : α), b = c * a → P) : P

@[simp]

theorem dvd_mul_left {α : Type u_1} [CommSemigroup α] (a : α) (b : α) : a ∣ b * a

theorem dvd_mul_of_dvd_right {α : Type u_1} [CommSemigroup α] {a : α} {b : α} (h : a ∣ b) (c : α) : a ∣ c * b

theorem Dvd.dvd.mul_left {α : Type u_1} [CommSemigroup α] {a : α} {b : α} (h : a ∣ b) (c : α) : a ∣ c * b

Alias of dvd_mul_of_dvd_right.

theorem mul_dvd_mul {α : Type u_1} [CommSemigroup α] {a : α} {b : α} {c : α} {d : α} : a ∣ b → c ∣ d → a * c ∣ b * d

theorem dvd_of_mul_left_dvd {α : Type u_1} [CommSemigroup α] {a : α} {b : α} {c : α} (h : a * b ∣ c) : b ∣ c

theorem dvd_mul {α : Type u_1} [CommSemigroup α] [DecompositionMonoid α] {k : α} {m : α} {n : α} : k ∣ m * n ↔ ∃ (d₁ : α), ∃ (d₂ : α), d₁ ∣ m ∧ d₂ ∣ n ∧ k = d₁ * d₂

theorem mul_dvd_mul_left {α : Type u_1} [CommMonoid α] (a : α) {b : α} {c : α} (h : b ∣ c) : a * b ∣ a * c

theorem mul_dvd_mul_right {α : Type u_1} [CommMonoid α] {a : α} {b : α} (h : a ∣ b) (c : α) : a * c ∣ b * c

theorem pow_dvd_pow_of_dvd {α : Type u_1} [CommMonoid α] {a : α} {b : α} (h : a ∣ b) (n : ℕ) : a ^ n ∣ b ^ n