doc-next-gen

Mathlib.Algebra.GroupWithZero.Divisibility

Module docstring

{"# Divisibility in groups with zero.

Lemmas about divisibility in groups and monoids with zero.

"}

zero_dvd_iff theorem
: 0 ∣ a ↔ a = 0
Full source 
/-- Given an element `a` of a commutative semigroup with zero, there exists another element whose
    product with zero equals `a` iff `a` equals zero. -/
@[simp]
theorem zero_dvd_iff : 0 ∣ a0 ∣ a ↔ a = 0 :=
  ⟨eq_zero_of_zero_dvd, fun h => by
    rw [h]
    exact ⟨0, by simp⟩⟩
Zero Divides Element if and only if Element is Zero
Informal description
For any element $a$ in a commutative semigroup with zero, the element $0$ divides $a$ if and only if $a = 0$.
dvd_zero theorem
(a : α) : a ∣ 0
Full source 
@[simp]
theorem dvd_zero (a : α) : a ∣ 0 :=
  Dvd.intro 0 (by simp)
Every Element Divides Zero in a Semigroup with Zero
Informal description
For any element $a$ in a semigroup with zero, $a$ divides $0$.
mul_dvd_mul_iff_left theorem
[CancelMonoidWithZero α] {a b c : α} (ha : a ≠ 0) : a * b ∣ a * c ↔ b ∣ c
Full source 
/-- Given two elements `b`, `c` of a `CancelMonoidWithZero` and a nonzero element `a`,
 `a*b` divides `a*c` iff `b` divides `c`. -/
theorem mul_dvd_mul_iff_left [CancelMonoidWithZero α] {a b c : α} (ha : a ≠ 0) :
    a * b ∣ a * ca * b ∣ a * c ↔ b ∣ c :=
  exists_congr fun d => by rw [mul_assoc, mul_right_inj' ha]
Left Cancellation Property for Divisibility in Cancellative Monoids with Zero: $a \cdot b \mid a \cdot c \leftrightarrow b \mid c$ for $a \neq 0$
Informal description
Let $\alpha$ be a cancellative monoid with zero. For any nonzero element $a \in \alpha$ and elements $b, c \in \alpha$, the product $a \cdot b$ divides $a \cdot c$ if and only if $b$ divides $c$.
mul_dvd_mul_iff_right theorem
[CancelCommMonoidWithZero α] {a b c : α} (hc : c ≠ 0) : a * c ∣ b * c ↔ a ∣ b
Full source 
/-- Given two elements `a`, `b` of a commutative `CancelMonoidWithZero` and a nonzero
  element `c`, `a*c` divides `b*c` iff `a` divides `b`. -/
theorem mul_dvd_mul_iff_right [CancelCommMonoidWithZero α] {a b c : α} (hc : c ≠ 0) :
    a * c ∣ b * ca * c ∣ b * c ↔ a ∣ b :=
  exists_congr fun d => by rw [mul_right_comm, mul_left_inj' hc]
Right Cancellation Property for Divisibility in Cancellative Commutative Monoids with Zero: $a \cdot c \mid b \cdot c \leftrightarrow a \mid b$ for $c \neq 0$
Informal description
Let $\alpha$ be a cancellative commutative monoid with zero. For any elements $a, b, c \in \alpha$ with $c \neq 0$, we have $a \cdot c \mid b \cdot c$ if and only if $a \mid b$.
DvdNotUnit definition
(a b : α) : Prop
Full source 
/-- `DvdNotUnit a b` expresses that `a` divides `b` "strictly", i.e. that `b` divided by `a`
is not a unit. -/
def DvdNotUnit (a b : α) : Prop :=
  a ≠ 0a ≠ 0 ∧ ∃ x, ¬IsUnit x ∧ b = a * x
Strict divisibility in monoids with zero
Informal description
For elements \( a \) and \( b \) in a monoid with zero, \( \text{DvdNotUnit} \, a \, b \) means that \( a \) divides \( b \) strictly, i.e., \( a \neq 0 \) and there exists an element \( x \) such that \( x \) is not a unit and \( b = a \cdot x \).
dvdNotUnit_of_dvd_of_not_dvd theorem
{a b : α} (hd : a ∣ b) (hnd : ¬b ∣ a) : DvdNotUnit a b
Full source 
theorem dvdNotUnit_of_dvd_of_not_dvd {a b : α} (hd : a ∣ b) (hnd : ¬b ∣ a) : DvdNotUnit a b := by
  constructor
  · rintro rfl
    exact hnd (dvd_zero _)
  · rcases hd with ⟨c, rfl⟩
    refine ⟨c, ?_, rfl⟩
    rintro ⟨u, rfl⟩
    simp at hnd
Strict Divisibility from Non-Symmetric Divisibility in Monoids with Zero
Informal description
For any elements $a$ and $b$ in a monoid with zero, if $a$ divides $b$ but $b$ does not divide $a$, then $a$ strictly divides $b$ (i.e., $a \neq 0$ and there exists a non-unit element $x$ such that $b = a \cdot x$).
IsRelPrime.ne_zero_or_ne_zero theorem
[Nontrivial α] (h : IsRelPrime x y) : x ≠ 0 ∨ y ≠ 0
Full source 
theorem IsRelPrime.ne_zero_or_ne_zero [Nontrivial α] (h : IsRelPrime x y) : x ≠ 0x ≠ 0 ∨ y ≠ 0 :=
  not_or_of_imp <| by rintro rfl rfl; exact not_isRelPrime_zero_zero h
Relatively Prime Elements Have Nonzero Pair in Nontrivial Monoid with Zero
Informal description
Let $\alpha$ be a nontrivial monoid with zero. If two elements $x, y \in \alpha$ are relatively prime, then at least one of them is nonzero, i.e., $x \neq 0$ or $y \neq 0$.
isRelPrime_of_no_nonunits_factors theorem
[MonoidWithZero α] {x y : α} (nonzero : ¬(x = 0 ∧ y = 0)) (H : ∀ z, ¬IsUnit z → z ≠ 0 → z ∣ x → ¬z ∣ y) : IsRelPrime x y
Full source 
theorem isRelPrime_of_no_nonunits_factors [MonoidWithZero α] {x y : α} (nonzero : ¬(x = 0 ∧ y = 0))
    (H : ∀ z, ¬ IsUnit z → z ≠ 0 → z ∣ x → ¬z ∣ y) : IsRelPrime x y := by
  refine fun z hx hy ↦ by_contra fun h ↦ H z h ?_ hx hy
  rintro rfl; exact nonzero ⟨zero_dvd_iff.1 hx, zero_dvd_iff.1 hy⟩
Relatively Prime Elements via Non-Unit Divisors
Informal description
Let $\alpha$ be a monoid with zero, and let $x, y \in \alpha$ such that it is not the case that both $x = 0$ and $y = 0$. Suppose that for every non-unit element $z \neq 0$ in $\alpha$, if $z$ divides $x$ then $z$ does not divide $y$. Then $x$ and $y$ are relatively prime.
dvd_and_not_dvd_iff theorem
[CancelCommMonoidWithZero α] {x y : α} : x ∣ y ∧ ¬y ∣ x ↔ DvdNotUnit x y
Full source 
theorem dvd_and_not_dvd_iff [CancelCommMonoidWithZero α] {x y : α} :
    x ∣ yx ∣ y ∧ ¬y ∣ xx ∣ y ∧ ¬y ∣ x ↔ DvdNotUnit x y :=
  ⟨fun ⟨⟨d, hd⟩, hyx⟩ =>
    ⟨fun hx0 => by simp [hx0] at hyx,
      ⟨d, mt isUnit_iff_dvd_one.1 fun ⟨e, he⟩ => hyx ⟨e, by rw [hd, mul_assoc, ← he, mul_one]⟩,
        hd⟩⟩,
    fun ⟨hx0, d, hdu, hdx⟩ =>
    ⟨⟨d, hdx⟩, fun ⟨e, he⟩ =>
      hdu
        (isUnit_of_dvd_one
          ⟨e, mul_left_cancel₀ hx0 <| by conv =>
            lhs
            rw [he, hdx]
            simp [mul_assoc]⟩)⟩⟩
Characterization of Strict Divisibility in Cancellative Commutative Monoids with Zero
Informal description
Let $\alpha$ be a cancellative commutative monoid with zero. For any elements $x, y \in \alpha$, the following are equivalent: 1. $x$ divides $y$ and $y$ does not divide $x$. 2. $x$ strictly divides $y$, i.e., $x \neq 0$ and there exists a non-unit element $z$ such that $y = x \cdot z$.
ne_zero_of_dvd_ne_zero theorem
{p q : α} (h₁ : q ≠ 0) (h₂ : p ∣ q) : p ≠ 0
Full source 
theorem ne_zero_of_dvd_ne_zero {p q : α} (h₁ : q ≠ 0) (h₂ : p ∣ q) : p ≠ 0 := by
  rcases h₂ with ⟨u, rfl⟩
  exact left_ne_zero_of_mul h₁
Nonzero Divisor of Nonzero Element is Nonzero
Informal description
For any elements $p$ and $q$ in a monoid with zero, if $q$ is nonzero and $p$ divides $q$, then $p$ is nonzero.
isPrimal_zero theorem
: IsPrimal (0 : α)
Full source 
theorem isPrimal_zero : IsPrimal (0 : α) :=
  fun a b h ↦ ⟨a, b, dvd_rfl, dvd_rfl, (zero_dvd_iff.mp h).symm⟩
Zero is Primal in Cancellative Commutative Monoids with Zero
Informal description
The zero element $0$ in a cancellative commutative monoid with zero $\alpha$ is primal. That is, for any elements $b, c \in \alpha$ such that $0$ divides $b \cdot c$, there exist elements $a_1, a_2 \in \alpha$ such that $a_1$ divides $b$, $a_2$ divides $c$, and $0 = a_1 \cdot a_2$.
IsPrimal.mul theorem
{α} [CancelCommMonoidWithZero α] {m n : α} (hm : IsPrimal m) (hn : IsPrimal n) : IsPrimal (m * n)
Full source 
theorem IsPrimal.mul {α} [CancelCommMonoidWithZero α] {m n : α}
    (hm : IsPrimal m) (hn : IsPrimal n) : IsPrimal (m * n) := by
  obtain rfl | h0 := eq_or_ne m 0; · rwa [zero_mul]
  intro b c h
  obtain ⟨a₁, a₂, ⟨b, rfl⟩, ⟨c, rfl⟩, rfl⟩ := hm (dvd_of_mul_right_dvd h)
  rw [mul_mul_mul_comm, mul_dvd_mul_iff_left h0] at h
  obtain ⟨a₁', a₂', h₁, h₂, rfl⟩ := hn h
  exact ⟨a₁ * a₁', a₂ * a₂', mul_dvd_mul_left _ h₁, mul_dvd_mul_left _ h₂, mul_mul_mul_comm _ _ _ _⟩
Product of Primal Elements is Primal in Cancellative Commutative Monoids with Zero
Informal description
Let $\alpha$ be a cancellative commutative monoid with zero. If elements $m$ and $n$ in $\alpha$ are primal, then their product $m \cdot n$ is also primal. That is, for any elements $b, c \in \alpha$ such that $m \cdot n$ divides $b \cdot c$, there exist elements $a_1, a_2 \in \alpha$ where $a_1$ divides $b$, $a_2$ divides $c$, and $m \cdot n = a_1 \cdot a_2$.
dvd_antisymm theorem
: a ∣ b → b ∣ a → a = b
Full source 
theorem dvd_antisymm : a ∣ b → b ∣ a → a = b := by
  rintro ⟨c, rfl⟩ ⟨d, hcd⟩
  rw [mul_assoc, eq_comm, mul_right_eq_self₀, mul_eq_one] at hcd
  obtain ⟨rfl, -⟩ | rfl := hcd <;> simp
Antisymmetry of Divisibility in Cancellative Commutative Monoids with Zero
Informal description
For any elements $a$ and $b$ in a cancellative commutative monoid with zero, if $a$ divides $b$ and $b$ divides $a$, then $a = b$.
dvd_antisymm' theorem
: a ∣ b → b ∣ a → b = a
Full source 
theorem dvd_antisymm' : a ∣ b → b ∣ a → b = a :=
  flip dvd_antisymm
Antisymmetry of Divisibility (Symmetric Form)
Informal description
For any elements $a$ and $b$ in a cancellative commutative monoid with zero, if $a$ divides $b$ and $b$ divides $a$, then $b = a$.
pow_dvd_pow_iff theorem
(ha₀ : a ≠ 0) (ha : ¬IsUnit a) : a ^ n ∣ a ^ m ↔ n ≤ m
Full source 
lemma pow_dvd_pow_iff (ha₀ : a ≠ 0) (ha : ¬IsUnit a) : a ^ n ∣ a ^ ma ^ n ∣ a ^ m ↔ n ≤ m := by
  constructor
  · intro h
    rw [← not_lt]
    intro hmn
    apply ha
    have : a ^ m * a ∣ a ^ m * 1 := by
      rw [← pow_succ, mul_one]
      exact (pow_dvd_pow _ (Nat.succ_le_of_lt hmn)).trans h
    rwa [mul_dvd_mul_iff_left, ← isUnit_iff_dvd_one] at this
    apply pow_ne_zero m ha₀
  · apply pow_dvd_pow
Power Divisibility Criterion: $a^n \mid a^m \leftrightarrow n \leq m$ for non-unit $a \neq 0$
Informal description
Let $\alpha$ be a cancellative commutative monoid with zero. For any nonzero element $a \in \alpha$ that is not a unit, and for any natural numbers $n$ and $m$, the power $a^n$ divides $a^m$ if and only if $n \leq m$.
GroupWithZero.dvd_iff theorem
{m n : α} : m ∣ n ↔ (m = 0 → n = 0)
Full source 
/-- `∣` is not a useful definition if an inverse is available. -/
@[simp]
lemma GroupWithZero.dvd_iff {m n : α} : m ∣ nm ∣ n ↔ (m = 0 → n = 0) := by
  refine ⟨fun ⟨a, ha⟩ hm => ?_, fun h => ?_⟩
  · simp [hm, ha]
  · refine ⟨m⁻¹ * n, ?_⟩
    obtain rfl | hn := eq_or_ne n 0
    · simp
    · rw [mul_inv_cancel_left₀ (mt h hn)]
Divisibility Criterion in Groups with Zero: $m \mid n \leftrightarrow (m = 0 \to n = 0)$
Informal description
For any elements $m$ and $n$ in a group with zero $\alpha$, the divisibility relation $m \mid n$ holds if and only if whenever $m = 0$, it must also be that $n = 0$.