Lemmas about divisibility and units #

source

theorem Units.coe_dvd {α : Type u_1} [Monoid α] {a : α} {u : αˣ} :

↑u ∣ a

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

source

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.

source

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.

source

theorem Units.dvd_mul_left {α : Type u_1} [CommMonoid α] {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.

source

theorem Units.mul_left_dvd {α : Type u_1} [CommMonoid α] {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.

source

@[simp]

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

u ∣ a

Units of a monoid divide any element of the monoid.

source

@[simp]

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

a ∣ b * u ↔ a ∣ b

source

@[simp]

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

a * u ∣ b ↔ a ∣ b

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

source

@[simp]

theorem IsUnit.dvd_mul_left {α : Type u_1} [CommMonoid α] (a : α) (b : α) (u : α) (hu : IsUnit 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.

source

@[simp]

theorem IsUnit.mul_left_dvd {α : Type u_1} [CommMonoid α] (a : α) (b : α) (u : α) (hu : IsUnit 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.

source

theorem isUnit_iff_dvd_one {α : Type u_1} [CommMonoid α] {x : α} :

IsUnit x ↔ x ∣ 1

source

theorem isUnit_iff_forall_dvd {α : Type u_1} [CommMonoid α] {x : α} :

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

source

theorem isUnit_of_dvd_unit {α : Type u_1} [CommMonoid α] {x : α} {y : α} (xy : x ∣ y) (hu : IsUnit y) :

IsUnit x

source

theorem isUnit_of_dvd_one {α : Type u_1} [CommMonoid α] {a : α} (h : a ∣ 1) :

IsUnit a

source

theorem not_isUnit_of_not_isUnit_dvd {α : Type u_1} [CommMonoid α] {a : α} {b : α} (ha : ¬IsUnit a) (hb : a ∣ b) :

¬IsUnit b