mathlib documentation

algebra.divisibility

Divisibility #

This file defines the basics of the divisibility relation in the context of (comm_) monoids (_with_zero).

Main definitions #

monoid.has_dvd

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

@[protected, instance]

def semigroup_has_dvd {α : Type u_1} [semigroup α] :

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

Equations

semigroup_has_dvd = {dvd := λ (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.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 has_dvd.dvd.trans {α : Type u_1} [semigroup α] {a b c : α} :

a ∣ b → b ∣ c → a ∣ c

Alias of dvd_trans.

@[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 has_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} [monoid M] [monoid N] {F : Type u_1} [mul_hom_class F M N] (f : F) {a b : M} :

a ∣ b → ⇑f a ∣ ⇑f b

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

a ∣ b → ⇑f a ∣ ⇑f b

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

a ∣ b → ⇑f a ∣ ⇑f b

@[simp]

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

a ∣ a

theorem dvd_rfl {α : Type u_1} [monoid α] {a : α} :

a ∣ a

theorem one_dvd {α : Type u_1} [monoid α] (a : α) :

1 ∣ a

theorem dvd.intro_left {α : Type u_1} [comm_semigroup α] {a b : α} (c : α) (h : c * a = b) :

a ∣ b

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

a ∣ b

Alias of dvd.intro_left.

theorem exists_eq_mul_left_of_dvd {α : Type u_1} [comm_semigroup α] {a b : α} (h : a ∣ b) :

∃ (c : α), b = c * a

theorem dvd_iff_exists_eq_mul_left {α : Type u_1} [comm_semigroup α] {a b : α} :

a ∣ b ↔ ∃ (c : α), b = c * a

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

P

@[simp]

theorem dvd_mul_left {α : Type u_1} [comm_semigroup α] (a b : α) :

a ∣ b * a

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

a ∣ c * b

theorem has_dvd.dvd.mul_left {α : Type u_1} [comm_semigroup α] {a b : α} (h : a ∣ b) (c : α) :

a ∣ c * b

Alias of dvd_mul_of_dvd_right.

theorem mul_dvd_mul {α : Type u_1} [comm_semigroup α] {a b c d : α} :

a ∣ b → c ∣ d → a * c ∣ b * d

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

b ∣ c

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

a * b ∣ a * c

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

a * c ∣ b * c

theorem eq_zero_of_zero_dvd {α : Type u_1} [semigroup_with_zero α] {a : α} (h : 0 ∣ a) :

a = 0

@[simp]

theorem zero_dvd_iff {α : Type u_1} [semigroup_with_zero α] {a : α} :

0 ∣ a ↔ a = 0

Given an element a of a commutative semigroup with zero, there exists another element whose product with zero equals a iff a equals zero.

@[simp]

theorem dvd_zero {α : Type u_1} [semigroup_with_zero α] (a : α) :

a ∣ 0

theorem mul_dvd_mul_iff_left {α : Type u_1} [cancel_monoid_with_zero α] {a b c : α} (ha : a ≠ 0) :

a * b ∣ a * c ↔ b ∣ c

Given two elements b, c of a cancel_monoid_with_zero and a nonzero element a, a*b divides a*c iff b divides c.

theorem mul_dvd_mul_iff_right {α : Type u_1} [cancel_comm_monoid_with_zero α] {a b c : α} (hc : c ≠ 0) :

a * c ∣ b * c ↔ a ∣ b

Given two elements a, b of a commutative cancel_monoid_with_zero and a nonzero element c, a*c divides b*c iff a divides b.

Units in various monoids #

theorem units.coe_dvd {α : Type u_1} [monoid α] {a : α} {u : αˣ} :

Elements of the unit group of a monoid represented as elements of the monoid divide any element of the monoid.

theorem units.dvd_mul_right {α : Type u_1} [monoid α] {a b : α} {u : αˣ} :

a ∣ b * ↑u ↔ a ∣ b

In a monoid, an element a divides an element b iff a divides all associates of b.

theorem units.mul_right_dvd {α : Type u_1} [monoid α] {a b : α} {u : αˣ} :

a * ↑u ∣ b ↔ a ∣ b

In a monoid, an element a divides an element b iff all associates of a divide b.

theorem units.dvd_mul_left {α : Type u_1} [comm_monoid α] {a b : α} {u : αˣ} :

a ∣ (↑u) * b ↔ a ∣ b

In a commutative monoid, an element a divides an element b iff a divides all left associates of b.

theorem units.mul_left_dvd {α : Type u_1} [comm_monoid α] {a b : α} {u : αˣ} :

(↑u) * a ∣ b ↔ a ∣ b

In a commutative monoid, an element a divides an element b iff all left associates of a divide b.

@[simp]

theorem is_unit.dvd {α : Type u_1} [monoid α] {a u : α} (hu : is_unit u) :

u ∣ a

Units of a monoid divide any element of the monoid.

@[simp]

theorem is_unit.dvd_mul_right {α : Type u_1} [monoid α] {a b u : α} (hu : is_unit u) :

a ∣ b * u ↔ a ∣ b

@[simp]

theorem is_unit.mul_right_dvd {α : Type u_1} [monoid α] {a b u : α} (hu : is_unit u) :

a * u ∣ b ↔ a ∣ b

In a monoid, an element a divides an element b iff all associates of a divide b.

@[simp]

theorem is_unit.dvd_mul_left {α : Type u_1} [comm_monoid α] (a b u : α) (hu : is_unit u) :

a ∣ u * b ↔ a ∣ b

In a commutative monoid, an element a divides an element b iff a divides all left associates of b.

@[simp]

theorem is_unit.mul_left_dvd {α : Type u_1} [comm_monoid α] (a b u : α) (hu : is_unit u) :

u * a ∣ b ↔ a ∣ b

In a commutative monoid, an element a divides an element b iff all left associates of a divide b.

theorem is_unit_iff_dvd_one {α : Type u_1} [comm_monoid α] {x : α} :

is_unit x ↔ x ∣ 1

theorem is_unit_iff_forall_dvd {α : Type u_1} [comm_monoid α] {x : α} :

is_unit x ↔ ∀ (y : α), x ∣ y

theorem is_unit_of_dvd_unit {α : Type u_1} [comm_monoid α] {x y : α} (xy : x ∣ y) (hu : is_unit y) :

theorem is_unit_of_dvd_one {α : Type u_1} [comm_monoid α] (a : α) (H : a ∣ 1) :

theorem not_is_unit_of_not_is_unit_dvd {α : Type u_1} [comm_monoid α] {a b : α} (ha : ¬is_unit a) (hb : a ∣ b) :

def dvd_not_unit {α : Type u_1} [comm_monoid_with_zero α] (a b : α) :

Prop

dvd_not_unit a b expresses that a divides b "strictly", i.e. that b divided by a is not a unit.

Equations

dvd_not_unit a b = (a ≠ 0 ∧ ∃ (x : α), ¬is_unit x ∧ b = a * x)

theorem dvd_not_unit_of_dvd_of_not_dvd {α : Type u_1} [comm_monoid_with_zero α] {a b : α} (hd : a ∣ b) (hnd : ¬b ∣ a) :

dvd_not_unit a b

theorem dvd_and_not_dvd_iff {α : Type u_1} [cancel_comm_monoid_with_zero α] {x y : α} :

x ∣ y ∧ ¬y ∣ x ↔ dvd_not_unit x y

theorem ne_zero_of_dvd_ne_zero {α : Type u_1} [monoid_with_zero α] {p q : α} (h₁ : q ≠ 0) (h₂ : p ∣ q) :

p ≠ 0