Divisibility and units #

Main definition #

• IsRelPrime x y: that x and y are relatively prime, defined to mean that the only common divisors of x and y are the units.
theorem Units.coe_dvd {α : Type u_1} [] {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} [] {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} [] {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} [] {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} [] {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 IsUnit.dvd {α : Type u_1} [] {a : α} {u : α} (hu : ) :
u a

Units of a monoid divide any element of the monoid.

@[simp]
theorem IsUnit.dvd_mul_right {α : Type u_1} [] {a : α} {b : α} {u : α} (hu : ) :
a b * u a b
@[simp]
theorem IsUnit.mul_right_dvd {α : Type u_1} [] {a : α} {b : α} {u : α} (hu : ) :
a * u b a b

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

theorem IsUnit.isPrimal {α : Type u_1} [] {u : α} (hu : ) :
@[simp]
theorem IsUnit.dvd_mul_left {α : Type u_1} [] {a : α} {b : α} {u : α} (hu : ) :
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 IsUnit.mul_left_dvd {α : Type u_1} [] {a : α} {b : α} {u : α} (hu : ) :
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 isUnit_iff_dvd_one {α : Type u_1} [] {x : α} :
x 1
theorem isUnit_iff_forall_dvd {α : Type u_1} [] {x : α} :
∀ (y : α), x y
theorem isUnit_of_dvd_unit {α : Type u_1} [] {x : α} {y : α} (xy : x y) (hu : ) :
theorem isUnit_of_dvd_one {α : Type u_1} [] {a : α} (h : a 1) :
theorem not_isUnit_of_not_isUnit_dvd {α : Type u_1} [] {a : α} {b : α} (ha : ¬) (hb : a b) :
def IsRelPrime {α : Type u_1} [] (x : α) (y : α) :

x and y are relatively prime if every common divisor is a unit.

Equations
• = ∀ ⦃d : α⦄, d xd y
Instances For
theorem IsRelPrime.symm {α : Type u_1} [] {x : α} {y : α} (H : ) :
theorem isRelPrime_comm {α : Type u_1} [] {x : α} {y : α} :
theorem isRelPrime_self {α : Type u_1} [] {x : α} :
theorem IsUnit.isRelPrime_left {α : Type u_1} [] {x : α} {y : α} (h : ) :
theorem IsUnit.isRelPrime_right {α : Type u_1} [] {x : α} {y : α} (h : ) :
theorem isRelPrime_one_left {α : Type u_1} [] {x : α} :
theorem isRelPrime_one_right {α : Type u_1} [] {x : α} :
theorem IsRelPrime.of_mul_left_left {α : Type u_1} [] {x : α} {y : α} {z : α} (H : IsRelPrime (x * y) z) :
theorem IsRelPrime.of_mul_left_right {α : Type u_1} [] {x : α} {y : α} {z : α} (H : IsRelPrime (x * y) z) :
theorem IsRelPrime.of_mul_right_left {α : Type u_1} [] {x : α} {y : α} {z : α} (H : IsRelPrime x (y * z)) :
theorem IsRelPrime.of_mul_right_right {α : Type u_1} [] {x : α} {y : α} {z : α} (H : IsRelPrime x (y * z)) :
theorem IsRelPrime.of_dvd_left {α : Type u_1} [] {x : α} {y : α} {z : α} (h : ) (dvd : x y) :
theorem IsRelPrime.of_dvd_right {α : Type u_1} [] {x : α} {y : α} {z : α} (h : ) (dvd : x y) :
theorem IsRelPrime.isUnit_of_dvd {α : Type u_1} [] {x : α} {y : α} (H : ) (d : x y) :
theorem isRelPrime_mul_unit_left_left {α : Type u_1} [] {x : α} {y : α} {z : α} (hu : ) :
IsRelPrime (x * y) z
theorem isRelPrime_mul_unit_left_right {α : Type u_1} [] {x : α} {y : α} {z : α} (hu : ) :
IsRelPrime y (x * z)
theorem isRelPrime_mul_unit_left {α : Type u_1} [] {x : α} {y : α} {z : α} (hu : ) :
IsRelPrime (x * y) (x * z)
theorem isRelPrime_mul_unit_right_left {α : Type u_1} [] {x : α} {y : α} {z : α} (hu : ) :
IsRelPrime (y * x) z
theorem isRelPrime_mul_unit_right_right {α : Type u_1} [] {x : α} {y : α} {z : α} (hu : ) :
IsRelPrime y (z * x)
theorem isRelPrime_mul_unit_right {α : Type u_1} [] {x : α} {y : α} {z : α} (hu : ) :
IsRelPrime (y * x) (z * x)
theorem IsRelPrime.dvd_of_dvd_mul_right_of_isPrimal {α : Type u_1} [] {x : α} {y : α} {z : α} (H1 : ) (H2 : x y * z) (h : ) :
x y
theorem IsRelPrime.dvd_of_dvd_mul_left_of_isPrimal {α : Type u_1} [] {x : α} {y : α} {z : α} (H1 : ) (H2 : x y * z) (h : ) :
x z
theorem IsRelPrime.mul_dvd_of_right_isPrimal {α : Type u_1} [] {x : α} {y : α} {z : α} (H : ) (H1 : x z) (H2 : y z) (hy : ) :
x * y z
theorem IsRelPrime.mul_dvd_of_left_isPrimal {α : Type u_1} [] {x : α} {y : α} {z : α} (H : ) (H1 : x z) (H2 : y z) (hx : ) :
x * y z

IsRelPrime enjoys desirable properties in a decomposition monoid. See Lemma 6.3 in On properties of square-free elements in commutative cancellative monoids, https://doi.org/10.1007/s00233-019-10022-3.

theorem IsRelPrime.dvd_of_dvd_mul_right {α : Type u_1} [] {x : α} {y : α} {z : α} (H1 : ) (H2 : x y * z) :
x y
theorem IsRelPrime.dvd_of_dvd_mul_left {α : Type u_1} [] {x : α} {y : α} {z : α} (H1 : ) (H2 : x y * z) :
x z
theorem IsRelPrime.mul_left {α : Type u_1} [] {x : α} {y : α} {z : α} (H1 : ) (H2 : ) :
IsRelPrime (x * y) z
theorem IsRelPrime.mul_right {α : Type u_1} [] {x : α} {y : α} {z : α} (H1 : ) (H2 : ) :
IsRelPrime x (y * z)
theorem IsRelPrime.mul_left_iff {α : Type u_1} [] {x : α} {y : α} {z : α} :
IsRelPrime (x * y) z
theorem IsRelPrime.mul_right_iff {α : Type u_1} [] {x : α} {y : α} {z : α} :
IsRelPrime x (y * z)
theorem IsRelPrime.mul_dvd {α : Type u_1} [] {x : α} {y : α} {z : α} (H : ) (H1 : x z) (H2 : y z) :
x * y z