Mathlib.Algebra.Divisibility.Units

Units.coe_dvd theorem

: ↑u ∣ a

Full source

/-- Elements of the unit group of a monoid represented as elements of the monoid
    divide any element of the monoid. -/
theorem coe_dvd : ↑u ∣ a :=
  ⟨↑u⁻¹ * a, by simp⟩

Units Divide All Elements in a Monoid

Informal description

For any unit $u$ in the group of units $\alpha^\times$ of a monoid $\alpha$ and any element $a \in \alpha$, the element $u$ (when viewed as an element of $\alpha$) divides $a$.

Units.dvd_mul_right theorem

: a ∣ b * u ↔ a ∣ b

Full source

/-- In a monoid, an element `a` divides an element `b` iff `a` divides all
    associates of `b`. -/
theorem dvd_mul_right : a ∣ b * ua ∣ b * u ↔ a ∣ b :=
  Iff.intro (fun ⟨c, eq⟩ ↦ ⟨c * ↑u⁻¹, by rw [← mul_assoc, ← eq, Units.mul_inv_cancel_right]⟩)
    fun ⟨_, eq⟩ ↦ eq.symm ▸ (_root_.dvd_mul_right _ _).mul_right _

Divisibility by Product with Unit iff Divisibility by Base Element

Informal description

For any elements $a$ and $b$ in a monoid $\alpha$, and any unit $u$ in the group of units $\alpha^\times$, the element $a$ divides the product $b \cdot u$ if and only if $a$ divides $b$.

Units.mul_right_dvd theorem

: a * u ∣ b ↔ a ∣ b

Full source

/-- In a monoid, an element `a` divides an element `b` iff all associates of `a` divide `b`. -/
theorem mul_right_dvd : a * u ∣ ba * u ∣ b ↔ a ∣ b :=
  Iff.intro (fun ⟨c, eq⟩ => ⟨↑u * c, eq.trans (mul_assoc _ _ _)⟩) fun h =>
    dvd_trans (Dvd.intro (↑u⁻¹) (by rw [mul_assoc, u.mul_inv, mul_one])) h

Divisibility by Product with Unit iff Divisibility by First Factor

Informal description

For any element $a$ and unit $u$ in a monoid, and any element $b$ in the same monoid, the product $a \cdot u$ divides $b$ if and only if $a$ divides $b$.

Units.dvd_mul_left theorem

: a ∣ u * b ↔ a ∣ b

Full source

/-- In a commutative monoid, an element `a` divides an element `b` iff `a` divides all left
    associates of `b`. -/
theorem dvd_mul_left : a ∣ u * ba ∣ u * b ↔ a ∣ b := by
  rw [mul_comm]
  apply dvd_mul_right

Divisibility by Product with Unit on Left iff Divisibility by Base Element

Informal description

For any elements $a$ and $b$ in a monoid $\alpha$, and any unit $u$ in the group of units $\alpha^\times$, the element $a$ divides the product $u \cdot b$ if and only if $a$ divides $b$.

Units.mul_left_dvd theorem

: ↑u * a ∣ b ↔ a ∣ b

Full source

/-- In a commutative monoid, an element `a` divides an element `b` iff all
  left associates of `a` divide `b`. -/
theorem mul_left_dvd : ↑u * a ∣ b↑u * a ∣ b ↔ a ∣ b := by
  rw [mul_comm]
  apply mul_right_dvd

Divisibility by Product with Unit on Left iff Divisibility by Second Factor

Informal description

For any element $a$ and unit $u$ in a commutative monoid, and any element $b$ in the same monoid, the product $u \cdot a$ divides $b$ if and only if $a$ divides $b$.

IsUnit.dvd theorem

(hu : IsUnit u) : u ∣ a

Full source

/-- Units of a monoid divide any element of the monoid. -/
@[simp]
theorem dvd (hu : IsUnit u) : u ∣ a := by
  rcases hu with ⟨u, rfl⟩
  apply Units.coe_dvd

Units Divide All Elements in a Monoid

Informal description

If $u$ is a unit in a monoid $M$, then $u$ divides every element $a \in M$.

IsUnit.dvd_mul_right theorem

(hu : IsUnit u) : a ∣ b * u ↔ a ∣ b

Full source

@[simp]
theorem dvd_mul_right (hu : IsUnit u) : a ∣ b * ua ∣ b * u ↔ a ∣ b := by
  rcases hu with ⟨u, rfl⟩
  apply Units.dvd_mul_right

Divisibility by Product with Unit iff Divisibility by Base Element

Informal description

For any elements $a$ and $b$ in a monoid $M$, and any unit $u \in M$, the element $a$ divides the product $b \cdot u$ if and only if $a$ divides $b$.

IsUnit.mul_right_dvd theorem

(hu : IsUnit u) : a * u ∣ b ↔ a ∣ b

Full source

/-- In a monoid, an element a divides an element b iff all associates of `a` divide `b`. -/
@[simp]
theorem mul_right_dvd (hu : IsUnit u) : a * u ∣ ba * u ∣ b ↔ a ∣ b := by
  rcases hu with ⟨u, rfl⟩
  apply Units.mul_right_dvd

Divisibility by Product with Unit iff Divisibility by First Factor

Informal description

For any element $a$ and unit $u$ in a monoid, and any element $b$ in the same monoid, the product $a \cdot u$ divides $b$ if and only if $a$ divides $b$.

IsUnit.isPrimal theorem

(hu : IsUnit u) : IsPrimal u

Full source

theorem isPrimal (hu : IsUnit u) : IsPrimal u :=
  fun _ _ _ ↦ ⟨u, 1, hu.dvd, one_dvd _, (mul_one u).symm⟩

Units are Primal in a Monoid

Informal description

If $u$ is a unit in a monoid $M$, then $u$ is a primal element in $M$.

IsUnit.dvd_mul_left theorem

(hu : IsUnit u) : a ∣ u * b ↔ a ∣ b

Full source

/-- In a commutative monoid, an element `a` divides an element `b` iff `a` divides all left
    associates of `b`. -/
@[simp]
theorem dvd_mul_left (hu : IsUnit u) : a ∣ u * ba ∣ u * b ↔ a ∣ b := by
  rcases hu with ⟨u, rfl⟩
  apply Units.dvd_mul_left

Divisibility by Unit Multiple: $a \mid u \cdot b \leftrightarrow a \mid b$ for unit $u$

Informal description

Let $M$ be a commutative monoid and let $u \in M$ be a unit. Then for any elements $a, b \in M$, the element $a$ divides the product $u \cdot b$ if and only if $a$ divides $b$.

IsUnit.mul_left_dvd theorem

(hu : IsUnit u) : u * a ∣ b ↔ a ∣ b

Full source

/-- In a commutative monoid, an element `a` divides an element `b` iff all
  left associates of `a` divide `b`. -/
@[simp]
theorem mul_left_dvd (hu : IsUnit u) : u * a ∣ bu * a ∣ b ↔ a ∣ b := by
  rcases hu with ⟨u, rfl⟩
  apply Units.mul_left_dvd

Divisibility by Unit Multiple: $u \cdot a \mid b \leftrightarrow a \mid b$ for unit $u$

Informal description

Let $M$ be a commutative monoid and let $u \in M$ be a unit. Then for any elements $a, b \in M$, the product $u \cdot a$ divides $b$ if and only if $a$ divides $b$.

isUnit_iff_dvd_one theorem

{x : α} : IsUnit x ↔ x ∣ 1

Full source

theorem isUnit_iff_dvd_one {x : α} : IsUnitIsUnit x ↔ x ∣ 1 :=
  ⟨IsUnit.dvd, fun ⟨y, h⟩ => ⟨⟨x, y, h.symm, by rw [h, mul_comm]⟩, rfl⟩⟩

Characterization of Units via Divisibility of One

Informal description

An element $x$ of a monoid $\alpha$ is a unit if and only if $x$ divides the multiplicative identity $1$.

isUnit_iff_forall_dvd theorem

{x : α} : IsUnit x ↔ ∀ y, x ∣ y

Full source

theorem isUnit_iff_forall_dvd {x : α} : IsUnitIsUnit x ↔ ∀ y, x ∣ y :=
  isUnit_iff_dvd_one.trans ⟨fun h _ => h.trans (one_dvd _), fun h => h _⟩

Characterization of Units via Universal Divisibility

Informal description

An element $x$ of a monoid $\alpha$ is a unit if and only if $x$ divides every element $y$ in $\alpha$.

isUnit_of_dvd_unit theorem

{x y : α} (xy : x ∣ y) (hu : IsUnit y) : IsUnit x

Full source

theorem isUnit_of_dvd_unit {x y : α} (xy : x ∣ y) (hu : IsUnit y) : IsUnit x :=
  isUnit_iff_dvd_one.2 <| xy.trans <| isUnit_iff_dvd_one.1 hu

Divisor of a Unit is a Unit

Informal description

Let $x$ and $y$ be elements of a monoid $\alpha$. If $x$ divides $y$ (i.e., $x \mid y$) and $y$ is a unit, then $x$ is also a unit.

isUnit_of_dvd_one theorem

{a : α} (h : a ∣ 1) : IsUnit (a : α)

Full source

theorem isUnit_of_dvd_one {a : α} (h : a ∣ 1) : IsUnit (a : α) :=
  isUnit_iff_dvd_one.mpr h

Elements Dividing One are Units

Informal description

For any element $a$ in a monoid $\alpha$, if $a$ divides the multiplicative identity $1$, then $a$ is a unit in $\alpha$.

not_isUnit_of_not_isUnit_dvd theorem

{a b : α} (ha : ¬IsUnit a) (hb : a ∣ b) : ¬IsUnit b

Full source

theorem not_isUnit_of_not_isUnit_dvd {a b : α} (ha : ¬IsUnit a) (hb : a ∣ b) : ¬IsUnit b :=
  mt (isUnit_of_dvd_unit hb) ha

Non-unit Divisor Implies Non-unit Dividend

Informal description

For any elements $a$ and $b$ in a monoid $\alpha$, if $a$ is not a unit and $a$ divides $b$, then $b$ is not a unit.

IsRelPrime definition

[Monoid α] (x y : α) : Prop

Full source

/-- `x` and `y` are relatively prime if every common divisor is a unit. -/
def IsRelPrime [Monoid α] (x y : α) : Prop := ∀ ⦃d⦄, d ∣ x → d ∣ y → IsUnit d

Relatively prime elements in a monoid

Informal description

Two elements $ x $ and $ y $ in a monoid $ \alpha $ are called *relatively prime* if every common divisor $ d $ of $ x $ and $ y $ is a unit in $ \alpha $. In other words, for any $ d $ such that $ d \mid x $ and $ d \mid y $, the element $ d $ must be invertible.

IsRelPrime.symm theorem

(H : IsRelPrime x y) : IsRelPrime y x

Full source

@[symm] theorem IsRelPrime.symm (H : IsRelPrime x y) : IsRelPrime y x := fun _ hx hy ↦ H hy hx

Symmetry of Relative Primality in a Monoid

Informal description

For any two elements $x$ and $y$ in a monoid, if $x$ and $y$ are relatively prime, then $y$ and $x$ are also relatively prime.

isRelPrime_comm theorem

: IsRelPrime x y ↔ IsRelPrime y x

Full source

theorem isRelPrime_comm : IsRelPrimeIsRelPrime x y ↔ IsRelPrime y x :=
  ⟨IsRelPrime.symm, IsRelPrime.symm⟩

Symmetry of Relative Primality: $\text{IsRelPrime}(x,y) \leftrightarrow \text{IsRelPrime}(y,x)$

Informal description

Two elements $x$ and $y$ in a monoid are relatively prime if and only if $y$ and $x$ are relatively prime. In other words, the relation of being relatively prime is symmetric.

isRelPrime_self theorem

: IsRelPrime x x ↔ IsUnit x

Full source

theorem isRelPrime_self : IsRelPrimeIsRelPrime x x ↔ IsUnit x :=
  ⟨(· dvd_rfl dvd_rfl), fun hu _ _ dvd ↦ isUnit_of_dvd_unit dvd hu⟩

Self-Relative-Primality Equivalence to Being a Unit

Informal description

An element $x$ in a monoid is relatively prime to itself if and only if $x$ is a unit. In other words, $\text{IsRelPrime}(x, x) \leftrightarrow \text{IsUnit}(x)$.

IsUnit.isRelPrime_left theorem

(h : IsUnit x) : IsRelPrime x y

Full source

theorem IsUnit.isRelPrime_left (h : IsUnit x) : IsRelPrime x y :=
  fun _ hx _ ↦ isUnit_of_dvd_unit hx h

Unit Elements are Relatively Prime to All Elements

Informal description

If an element $x$ in a monoid is a unit, then for any element $y$ in the same monoid, $x$ and $y$ are relatively prime.

IsUnit.isRelPrime_right theorem

(h : IsUnit y) : IsRelPrime x y

Full source

theorem IsUnit.isRelPrime_right (h : IsUnit y) : IsRelPrime x y := h.isRelPrime_left.symm

Unit Elements are Relatively Prime to All Elements (Right Version)

Informal description

If an element $y$ in a monoid is a unit, then for any element $x$ in the same monoid, $x$ and $y$ are relatively prime.

isRelPrime_one_left theorem

: IsRelPrime 1 x

Full source

theorem isRelPrime_one_left : IsRelPrime 1 x := isUnit_one.isRelPrime_left

Identity Element is Relatively Prime to All Elements

Informal description

In any monoid, the multiplicative identity element $1$ is relatively prime to any element $x$.

isRelPrime_one_right theorem

: IsRelPrime x 1

Full source

theorem isRelPrime_one_right : IsRelPrime x 1 := isUnit_one.isRelPrime_right

Relative Primality with Identity: $x$ and $1$ are Relatively Prime

Informal description

For any element $x$ in a monoid, $x$ and the multiplicative identity $1$ are relatively prime.

IsRelPrime.of_mul_left_left theorem

(H : IsRelPrime (x * y) z) : IsRelPrime x z

Full source

theorem IsRelPrime.of_mul_left_left (H : IsRelPrime (x * y) z) : IsRelPrime x z :=
  fun _ hx ↦ H (dvd_mul_of_dvd_left hx _)

Relative Primality Preserved Under Left Multiplication

Informal description

If the product $x \cdot y$ is relatively prime to $z$ in a monoid, then $x$ is relatively prime to $z$.

IsRelPrime.of_mul_left_right theorem

(H : IsRelPrime (x * y) z) : IsRelPrime y z

Full source

theorem IsRelPrime.of_mul_left_right (H : IsRelPrime (x * y) z) : IsRelPrime y z :=
  (mul_comm x y ▸ H).of_mul_left_left

Relative Primality Preserved Under Right Multiplication

Informal description

If the product $x \cdot y$ is relatively prime to $z$ in a monoid, then $y$ is relatively prime to $z$.

IsRelPrime.of_mul_right_left theorem

(H : IsRelPrime x (y * z)) : IsRelPrime x y

Full source

theorem IsRelPrime.of_mul_right_left (H : IsRelPrime x (y * z)) : IsRelPrime x y := by
  rw [isRelPrime_comm] at H ⊢
  exact H.of_mul_left_left

Relative Primality Preserved Under Right Multiplication (Left Factor)

Informal description

If $x$ is relatively prime to the product $y \cdot z$ in a monoid, then $x$ is relatively prime to $y$.

IsRelPrime.of_mul_right_right theorem

(H : IsRelPrime x (y * z)) : IsRelPrime x z

Full source

theorem IsRelPrime.of_mul_right_right (H : IsRelPrime x (y * z)) : IsRelPrime x z :=
  (mul_comm y z ▸ H).of_mul_right_left

Relative Primality Preserved Under Right Multiplication (Right Factor)

Informal description

For elements $x, y, z$ in a monoid, if $x$ is relatively prime to the product $y \cdot z$, then $x$ is relatively prime to $z$.

IsRelPrime.of_dvd_left theorem

(h : IsRelPrime y z) (dvd : x ∣ y) : IsRelPrime x z

Full source

theorem IsRelPrime.of_dvd_left (h : IsRelPrime y z) (dvd : x ∣ y) : IsRelPrime x z := by
  obtain ⟨d, rfl⟩ := dvd; exact IsRelPrime.of_mul_left_left h

Relative primality preserved under left division

Informal description

Let $x, y, z$ be elements of a monoid. If $y$ and $z$ are relatively prime and $x$ divides $y$, then $x$ and $z$ are relatively prime.

IsRelPrime.of_dvd_right theorem

(h : IsRelPrime z y) (dvd : x ∣ y) : IsRelPrime z x

Full source

theorem IsRelPrime.of_dvd_right (h : IsRelPrime z y) (dvd : x ∣ y) : IsRelPrime z x :=
  (h.symm.of_dvd_left dvd).symm

Relative primality preserved under right division

Informal description

Let $x, y, z$ be elements of a monoid. If $z$ and $y$ are relatively prime and $x$ divides $y$, then $z$ and $x$ are relatively prime.

IsRelPrime.isUnit_of_dvd theorem

(H : IsRelPrime x y) (d : x ∣ y) : IsUnit x

Full source

theorem IsRelPrime.isUnit_of_dvd (H : IsRelPrime x y) (d : x ∣ y) : IsUnit x := H dvd_rfl d

Relatively Prime Divisor Implies Unit

Informal description

If two elements $x$ and $y$ in a monoid are relatively prime and $x$ divides $y$, then $x$ is a unit.

isRelPrime_mul_unit_left_left theorem

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

Full source

theorem isRelPrime_mul_unit_left_left : IsRelPrimeIsRelPrime (x * y) z ↔ IsRelPrime y z :=
  ⟨IsRelPrime.of_mul_left_right, fun H _ h ↦ H (hu.dvd_mul_left.mp h)⟩

Relative Primality of Product: $\text{IsRelPrime}(x \cdot y, z) \leftrightarrow \text{IsRelPrime}(y, z)$

Informal description

Let $x, y, z$ be elements of a commutative monoid. Then the product $x \cdot y$ is relatively prime to $z$ if and only if $y$ is relatively prime to $z$.

isRelPrime_mul_unit_left_right theorem

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

Full source

theorem isRelPrime_mul_unit_left_right : IsRelPrimeIsRelPrime y (x * z) ↔ IsRelPrime y z := by
  rw [isRelPrime_comm, isRelPrime_mul_unit_left_left hu, isRelPrime_comm]

Relative Primality with Left Multiplication by Unit: $\text{IsRelPrime}(y, x \cdot z) \leftrightarrow \text{IsRelPrime}(y, z)$

Informal description

For elements $x, y, z$ in a commutative monoid, $y$ is relatively prime to the product $x \cdot z$ if and only if $y$ is relatively prime to $z$.

isRelPrime_mul_unit_left theorem

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

Full source

theorem isRelPrime_mul_unit_left : IsRelPrimeIsRelPrime (x * y) (x * z) ↔ IsRelPrime y z := by
  rw [isRelPrime_mul_unit_left_left hu, isRelPrime_mul_unit_left_right hu]

Relative Primality of Scaled Elements: $\text{IsRelPrime}(x \cdot y, x \cdot z) \leftrightarrow \text{IsRelPrime}(y, z)$

Informal description

For elements $x, y, z$ in a commutative monoid, the products $x \cdot y$ and $x \cdot z$ are relatively prime if and only if $y$ and $z$ are relatively prime.

isRelPrime_mul_unit_right_left theorem

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

Full source

theorem isRelPrime_mul_unit_right_left : IsRelPrimeIsRelPrime (y * x) z ↔ IsRelPrime y z := by
  rw [mul_comm, isRelPrime_mul_unit_left_left hu]

Relative Primality of Right Product: $\text{IsRelPrime}(y \cdot x, z) \leftrightarrow \text{IsRelPrime}(y, z)$

Informal description

For elements $x, y, z$ in a commutative monoid, the product $y \cdot x$ is relatively prime to $z$ if and only if $y$ is relatively prime to $z$.

isRelPrime_mul_unit_right_right theorem

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

Full source

theorem isRelPrime_mul_unit_right_right : IsRelPrimeIsRelPrime y (z * x) ↔ IsRelPrime y z := by
  rw [mul_comm, isRelPrime_mul_unit_left_right hu]

Relative Primality with Right Multiplication by Unit: $\text{IsRelPrime}(y, z \cdot x) \leftrightarrow \text{IsRelPrime}(y, z)$

Informal description

For elements $x, y, z$ in a commutative monoid, $y$ is relatively prime to the product $z \cdot x$ if and only if $y$ is relatively prime to $z$.

isRelPrime_mul_unit_right theorem

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

Full source

theorem isRelPrime_mul_unit_right : IsRelPrimeIsRelPrime (y * x) (z * x) ↔ IsRelPrime y z := by
  rw [isRelPrime_mul_unit_right_left hu, isRelPrime_mul_unit_right_right hu]

Relative Primality of Products with Common Unit Factor: $\text{IsRelPrime}(y \cdot x, z \cdot x) \leftrightarrow \text{IsRelPrime}(y, z)$

Informal description

For elements $x, y, z$ in a commutative monoid, the products $y \cdot x$ and $z \cdot x$ are relatively prime if and only if $y$ and $z$ are relatively prime.

IsRelPrime.dvd_of_dvd_mul_right_of_isPrimal theorem

(H1 : IsRelPrime x z) (H2 : x ∣ y * z) (h : IsPrimal x) : x ∣ y

Full source

theorem IsRelPrime.dvd_of_dvd_mul_right_of_isPrimal (H1 : IsRelPrime x z) (H2 : x ∣ y * z)
    (h : IsPrimal x) : x ∣ y := by
  obtain ⟨a, b, ha, hb, rfl⟩ := h H2
  exact (H1.of_mul_left_right.isUnit_of_dvd hb).mul_right_dvd.mpr ha

Primal Element Divides Right Factor When Relatively Prime to Left Factor

Informal description

Let $x$, $y$, and $z$ be elements of a commutative monoid $\alpha$. If $x$ and $z$ are relatively prime, $x$ divides $y \cdot z$, and $x$ is primal, then $x$ divides $y$.

IsRelPrime.dvd_of_dvd_mul_left_of_isPrimal theorem

(H1 : IsRelPrime x y) (H2 : x ∣ y * z) (h : IsPrimal x) : x ∣ z

Full source

theorem IsRelPrime.dvd_of_dvd_mul_left_of_isPrimal (H1 : IsRelPrime x y) (H2 : x ∣ y * z)
    (h : IsPrimal x) : x ∣ z :=
  H1.dvd_of_dvd_mul_right_of_isPrimal (mul_comm y z ▸ H2) h

Primal Element Divides Left Factor When Relatively Prime to Right Factor

Informal description

Let $x$, $y$, and $z$ be elements of a commutative monoid $\alpha$. If $x$ and $y$ are relatively prime, $x$ divides $y \cdot z$, and $x$ is primal, then $x$ divides $z$.

IsRelPrime.mul_dvd_of_right_isPrimal theorem

(H : IsRelPrime x y) (H1 : x ∣ z) (H2 : y ∣ z) (hy : IsPrimal y) : x * y ∣ z

Full source

theorem IsRelPrime.mul_dvd_of_right_isPrimal (H : IsRelPrime x y) (H1 : x ∣ z) (H2 : y ∣ z)
    (hy : IsPrimal y) : x * y ∣ z := by
  obtain ⟨w, rfl⟩ := H1
  exact mul_dvd_mul_left x (H.symm.dvd_of_dvd_mul_left_of_isPrimal H2 hy)

Product of Relatively Prime and Primal Elements Divides Common Multiple

Informal description

Let $x$, $y$, and $z$ be elements of a commutative monoid. If $x$ and $y$ are relatively prime, $x$ divides $z$, $y$ divides $z$, and $y$ is primal, then the product $x \cdot y$ divides $z$.

IsRelPrime.mul_dvd_of_left_isPrimal theorem

(H : IsRelPrime x y) (H1 : x ∣ z) (H2 : y ∣ z) (hx : IsPrimal x) : x * y ∣ z

Full source

theorem IsRelPrime.mul_dvd_of_left_isPrimal (H : IsRelPrime x y) (H1 : x ∣ z) (H2 : y ∣ z)
    (hx : IsPrimal x) : x * y ∣ z := by
  rw [mul_comm]; exact H.symm.mul_dvd_of_right_isPrimal H2 H1 hx

Product of Relatively Prime and Primal Elements Divides Common Multiple (Left Primal Variant)

Informal description

Let $x$, $y$, and $z$ be elements of a commutative monoid. If $x$ and $y$ are relatively prime, $x$ divides $z$, $y$ divides $z$, and $x$ is primal, then the product $x \cdot y$ divides $z$.

IsRelPrime.dvd_of_dvd_mul_right theorem

(H1 : IsRelPrime x z) (H2 : x ∣ y * z) : x ∣ y

Full source

theorem IsRelPrime.dvd_of_dvd_mul_right (H1 : IsRelPrime x z) (H2 : x ∣ y * z) : x ∣ y :=
  H1.dvd_of_dvd_mul_right_of_isPrimal H2 (DecompositionMonoid.primal x)

Relatively Prime Element Divides Right Factor: $(x \perp z) \land (x \mid y \cdot z) \Rightarrow (x \mid y)$

Informal description

Let $x$, $y$, and $z$ be elements of a monoid. If $x$ and $z$ are relatively prime and $x$ divides $y \cdot z$, then $x$ divides $y$.

IsRelPrime.dvd_of_dvd_mul_left theorem

(H1 : IsRelPrime x y) (H2 : x ∣ y * z) : x ∣ z

Full source

theorem IsRelPrime.dvd_of_dvd_mul_left (H1 : IsRelPrime x y) (H2 : x ∣ y * z) : x ∣ z :=
  H1.dvd_of_dvd_mul_right (mul_comm y z ▸ H2)

Relatively Prime Element Divides Left Factor: $(x \perp y) \land (x \mid y \cdot z) \Rightarrow (x \mid z)$

Informal description

Let $x$, $y$, and $z$ be elements of a monoid. If $x$ and $y$ are relatively prime and $x$ divides $y \cdot z$, then $x$ divides $z$.

IsRelPrime.mul_left theorem

(H1 : IsRelPrime x z) (H2 : IsRelPrime y z) : IsRelPrime (x * y) z

Full source

theorem IsRelPrime.mul_left (H1 : IsRelPrime x z) (H2 : IsRelPrime y z) : IsRelPrime (x * y) z :=
  fun _ h hz ↦ by
    obtain ⟨a, b, ha, hb, rfl⟩ := exists_dvd_and_dvd_of_dvd_mul h
    exact (H1 ha <| (dvd_mul_right a b).trans hz).mul (H2 hb <| (dvd_mul_left b a).trans hz)

Relatively Prime Elements Remain So Under Multiplication: $(x \perp z) \land (y \perp z) \Rightarrow (x \cdot y \perp z)$

Informal description

Let $x$, $y$, and $z$ be elements of a monoid. If $x$ is relatively prime to $z$ and $y$ is relatively prime to $z$, then their product $x \cdot y$ is also relatively prime to $z$.

IsRelPrime.mul_right theorem

(H1 : IsRelPrime x y) (H2 : IsRelPrime x z) : IsRelPrime x (y * z)

Full source

theorem IsRelPrime.mul_right (H1 : IsRelPrime x y) (H2 : IsRelPrime x z) :
    IsRelPrime x (y * z) := by
  rw [isRelPrime_comm] at H1 H2 ⊢; exact H1.mul_left H2

Relatively Prime Elements Remain So Under Right Multiplication: $(x \perp y) \land (x \perp z) \Rightarrow (x \perp y \cdot z)$

Informal description

Let $x$, $y$, and $z$ be elements of a monoid. If $x$ is relatively prime to $y$ and $x$ is relatively prime to $z$, then $x$ is relatively prime to the product $y \cdot z$.

IsRelPrime.mul_left_iff theorem

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

Full source

theorem IsRelPrime.mul_left_iff : IsRelPrimeIsRelPrime (x * y) z ↔ IsRelPrime x z ∧ IsRelPrime y z :=
  ⟨fun H ↦ ⟨H.of_mul_left_left, H.of_mul_left_right⟩, fun ⟨H1, H2⟩ ↦ H1.mul_left H2⟩

Characterization of Relative Primality Under Multiplication: $(x \cdot y \perp z) \leftrightarrow (x \perp z) \land (y \perp z)$

Informal description

For elements $x$, $y$, and $z$ in a monoid, the product $x \cdot y$ is relatively prime to $z$ if and only if both $x$ and $y$ are relatively prime to $z$ individually. In other words, $x \cdot y \perp z \leftrightarrow (x \perp z) \land (y \perp z)$.

IsRelPrime.mul_right_iff theorem

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

Full source

theorem IsRelPrime.mul_right_iff : IsRelPrimeIsRelPrime x (y * z) ↔ IsRelPrime x y ∧ IsRelPrime x z :=
  ⟨fun H ↦ ⟨H.of_mul_right_left, H.of_mul_right_right⟩, fun ⟨H1, H2⟩ ↦ H1.mul_right H2⟩

Characterization of Relative Primality Under Right Multiplication: $x \perp (y \cdot z) \leftrightarrow (x \perp y) \land (x \perp z)$

Informal description

For elements $x$, $y$, and $z$ in a monoid, $x$ is relatively prime to the product $y \cdot z$ if and only if $x$ is relatively prime to $y$ and $x$ is relatively prime to $z$ individually. In other words, $x \perp (y \cdot z) \leftrightarrow (x \perp y) \land (x \perp z)$.

IsRelPrime.mul_dvd theorem

(H : IsRelPrime x y) (H1 : x ∣ z) (H2 : y ∣ z) : x * y ∣ z

Full source

theorem IsRelPrime.mul_dvd (H : IsRelPrime x y) (H1 : x ∣ z) (H2 : y ∣ z) : x * y ∣ z :=
  H.mul_dvd_of_left_isPrimal H1 H2 (DecompositionMonoid.primal x)

Product of Relatively Prime Elements Divides Common Multiple

Informal description

Let $x$, $y$, and $z$ be elements of a commutative monoid. If $x$ and $y$ are relatively prime, and both $x$ and $y$ divide $z$, then the product $x \cdot y$ divides $z$.

Main definition