mathlib documentation

algebra.divisibility.units

Lemmas about divisibility and units #

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

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.

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 : α} :
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) :