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.

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

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

IsPrimal u

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

source

def IsRelPrime {α : Type u_1} [Monoid α] (x : α) (y : α) :

Prop

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

Equations

IsRelPrime x y = ∀ ⦃d : α⦄, d ∣ x → d ∣ y → IsUnit d

Instances For

source

theorem IsRelPrime.symm {α : Type u_1} [CommMonoid α] {x : α} {y : α} (H : IsRelPrime x y) :

IsRelPrime y x

source

theorem isRelPrime_comm {α : Type u_1} [CommMonoid α] {x : α} {y : α} :

IsRelPrime x y ↔ IsRelPrime y x

source

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

IsRelPrime x x ↔ IsUnit x

source

theorem IsUnit.isRelPrime_left {α : Type u_1} [CommMonoid α] {x : α} {y : α} (h : IsUnit x) :

IsRelPrime x y

source

theorem IsUnit.isRelPrime_right {α : Type u_1} [CommMonoid α] {x : α} {y : α} (h : IsUnit y) :

IsRelPrime x y

source

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

IsRelPrime 1 x

source

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

IsRelPrime x 1

source

theorem IsRelPrime.of_mul_left_left {α : Type u_1} [CommMonoid α] {x : α} {y : α} {z : α} (H : IsRelPrime (x * y) z) :

IsRelPrime x z

source

theorem IsRelPrime.of_mul_left_right {α : Type u_1} [CommMonoid α] {x : α} {y : α} {z : α} (H : IsRelPrime (x * y) z) :

IsRelPrime y z

source

theorem IsRelPrime.of_mul_right_left {α : Type u_1} [CommMonoid α] {x : α} {y : α} {z : α} (H : IsRelPrime x (y * z)) :

IsRelPrime x y

source

theorem IsRelPrime.of_mul_right_right {α : Type u_1} [CommMonoid α] {x : α} {y : α} {z : α} (H : IsRelPrime x (y * z)) :

IsRelPrime x z

source

theorem IsRelPrime.of_dvd_left {α : Type u_1} [CommMonoid α] {x : α} {y : α} {z : α} (h : IsRelPrime y z) (dvd : x ∣ y) :

IsRelPrime x z

source

theorem IsRelPrime.of_dvd_right {α : Type u_1} [CommMonoid α] {x : α} {y : α} {z : α} (h : IsRelPrime z y) (dvd : x ∣ y) :

IsRelPrime z x

source

theorem IsRelPrime.isUnit_of_dvd {α : Type u_1} [CommMonoid α] {x : α} {y : α} (H : IsRelPrime x y) (d : x ∣ y) :

IsUnit x

source

theorem isRelPrime_mul_unit_left_left {α : Type u_1} [CommMonoid α] {x : α} {y : α} {z : α} (hu : IsUnit x) :

IsRelPrime (x * y) z ↔ IsRelPrime y z

source

theorem isRelPrime_mul_unit_left_right {α : Type u_1} [CommMonoid α] {x : α} {y : α} {z : α} (hu : IsUnit x) :

IsRelPrime y (x * z) ↔ IsRelPrime y z

source

theorem isRelPrime_mul_unit_left {α : Type u_1} [CommMonoid α] {x : α} {y : α} {z : α} (hu : IsUnit x) :

IsRelPrime (x * y) (x * z) ↔ IsRelPrime y z

source

theorem isRelPrime_mul_unit_right_left {α : Type u_1} [CommMonoid α] {x : α} {y : α} {z : α} (hu : IsUnit x) :

IsRelPrime (y * x) z ↔ IsRelPrime y z

source

theorem isRelPrime_mul_unit_right_right {α : Type u_1} [CommMonoid α] {x : α} {y : α} {z : α} (hu : IsUnit x) :

IsRelPrime y (z * x) ↔ IsRelPrime y z

source

theorem isRelPrime_mul_unit_right {α : Type u_1} [CommMonoid α] {x : α} {y : α} {z : α} (hu : IsUnit x) :

IsRelPrime (y * x) (z * x) ↔ IsRelPrime y z

source

theorem IsRelPrime.dvd_of_dvd_mul_right_of_isPrimal {α : Type u_1} [CommMonoid α] {x : α} {y : α} {z : α} (H1 : IsRelPrime x z) (H2 : x ∣ y * z) (h : IsPrimal x) :

x ∣ y

source

theorem IsRelPrime.dvd_of_dvd_mul_left_of_isPrimal {α : Type u_1} [CommMonoid α] {x : α} {y : α} {z : α} (H1 : IsRelPrime x y) (H2 : x ∣ y * z) (h : IsPrimal x) :

x ∣ z

source

theorem IsRelPrime.mul_dvd_of_right_isPrimal {α : Type u_1} [CommMonoid α] {x : α} {y : α} {z : α} (H : IsRelPrime x y) (H1 : x ∣ z) (H2 : y ∣ z) (hy : IsPrimal y) :

x * y ∣ z

source

theorem IsRelPrime.mul_dvd_of_left_isPrimal {α : Type u_1} [CommMonoid α] {x : α} {y : α} {z : α} (H : IsRelPrime x y) (H1 : x ∣ z) (H2 : y ∣ z) (hx : IsPrimal x) :

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.

source

theorem IsRelPrime.dvd_of_dvd_mul_right {α : Type u_1} [CommMonoid α] {x : α} {y : α} {z : α} [DecompositionMonoid α] (H1 : IsRelPrime x z) (H2 : x ∣ y * z) :

x ∣ y

source

theorem IsRelPrime.dvd_of_dvd_mul_left {α : Type u_1} [CommMonoid α] {x : α} {y : α} {z : α} [DecompositionMonoid α] (H1 : IsRelPrime x y) (H2 : x ∣ y * z) :

x ∣ z

source

theorem IsRelPrime.mul_left {α : Type u_1} [CommMonoid α] {x : α} {y : α} {z : α} [DecompositionMonoid α] (H1 : IsRelPrime x z) (H2 : IsRelPrime y z) :

IsRelPrime (x * y) z

source

theorem IsRelPrime.mul_right {α : Type u_1} [CommMonoid α] {x : α} {y : α} {z : α} [DecompositionMonoid α] (H1 : IsRelPrime x y) (H2 : IsRelPrime x z) :

IsRelPrime x (y * z)

source

theorem IsRelPrime.mul_left_iff {α : Type u_1} [CommMonoid α] {x : α} {y : α} {z : α} [DecompositionMonoid α] :

IsRelPrime (x * y) z ↔ IsRelPrime x z ∧ IsRelPrime y z

source

theorem IsRelPrime.mul_right_iff {α : Type u_1} [CommMonoid α] {x : α} {y : α} {z : α} [DecompositionMonoid α] :

IsRelPrime x (y * z) ↔ IsRelPrime x y ∧ IsRelPrime x z

source

theorem IsRelPrime.mul_dvd {α : Type u_1} [CommMonoid α] {x : α} {y : α} {z : α} [DecompositionMonoid α] (H : IsRelPrime x y) (H1 : x ∣ z) (H2 : y ∣ z) :

x * y ∣ z

Documentation

Mathlib.Algebra.Divisibility.Units

Divisibility and units #

Main definition #