mathlib3 documentation

algebra.divisibility.basic

Divisibility #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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

@[trans]

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.

@[protected, instance]

def has_dvd.dvd.is_trans {α : Type u_1} [semigroup α] :

is_trans α has_dvd.dvd

@[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, refl]

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

a ∣ a

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

a ∣ a

@[protected, instance]

def has_dvd.dvd.is_refl {α : Type u_1} [monoid α] :

is_refl α has_dvd.dvd

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 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 pow_dvd_pow_of_dvd {α : Type u_1} [comm_monoid α] {a b : α} (h : a ∣ b) (n : ℕ) :

a ^ n ∣ b ^ n