# Divisibility in groups with zero. #

Lemmas about divisibility in groups and monoids with zero.

source
theorem eq_zero_of_zero_dvd {α : Type u_1} [SemigroupWithZero α] {a : α} (h : 0 ∣ a) :
a = 0
source
@[simp]
theorem zero_dvd_iff {α : Type u_1} [SemigroupWithZero α] {a : α} :
0 ∣ a ↔ a = 0

Given an element `a` of a commutative semigroup with zero, there exists another element whose product with zero equals `a` iff `a` equals zero.

source
@[simp]
theorem dvd_zero {α : Type u_1} [SemigroupWithZero α] (a : α) :
a ∣ 0
source
theorem mul_dvd_mul_iff_left {α : Type u_1} [CancelMonoidWithZero α] {a b c : α} (ha : a ≠ 0) :
a * b ∣ a * c ↔ b ∣ c

Given two elements `b`, `c` of a `CancelMonoidWithZero` and a nonzero element `a`, `a*b` divides `a*c` iff `b` divides `c`.

source
theorem mul_dvd_mul_iff_right {α : Type u_1} [CancelCommMonoidWithZero α] {a b c : α} (hc : c ≠ 0) :
a * c ∣ b * c ↔ a ∣ b

Given two elements `a`, `b` of a commutative `CancelMonoidWithZero` and a nonzero element `c`, `a*c` divides `b*c` iff `a` divides `b`.

source
def DvdNotUnit {α : Type u_1} [CommMonoidWithZero α] (a b : α) :
Prop

`DvdNotUnit a b` expresses that `a` divides `b` "strictly", i.e. that `b` divided by `a` is not a unit.

Equations

- DvdNotUnit a b = (a ≠ 0 ∧ ∃ (x : α), ¬IsUnit x ∧ b = a * x)

Instances For

source
theorem dvdNotUnit_of_dvd_of_not_dvd {α : Type u_1} [CommMonoidWithZero α] {a b : α} (hd : a ∣ b) (hnd : ¬b ∣ a) :
DvdNotUnit a b
source
theorem isRelPrime_zero_left {α : Type u_1} [CommMonoidWithZero α] {x : α} :
IsRelPrime 0 x ↔ IsUnit x
source
theorem isRelPrime_zero_right {α : Type u_1} [CommMonoidWithZero α] {x : α} :
IsRelPrime x 0 ↔ IsUnit x
source
theorem not_isRelPrime_zero_zero {α : Type u_1} [CommMonoidWithZero α] [Nontrivial α] :
¬IsRelPrime 0 0
source
theorem IsRelPrime.ne_zero_or_ne_zero {α : Type u_1} [CommMonoidWithZero α] {x y : α} [Nontrivial α] (h : IsRelPrime x y) :
x ≠ 0 ∨ y ≠ 0
source
theorem isRelPrime_of_no_nonunits_factors {α : Type u_1} [MonoidWithZero α] {x y : α} (nonzero : ¬(x = 0 ∧ y = 0)) (H : ∀ (z : α), ¬IsUnit z → z ≠ 0 → z ∣ x → ¬z ∣ y) :
IsRelPrime x y
source
theorem dvd_and_not_dvd_iff {α : Type u_1} [CancelCommMonoidWithZero α] {x y : α} :
x ∣ y ∧ ¬y ∣ x ↔ DvdNotUnit x y
source
theorem ne_zero_of_dvd_ne_zero {α : Type u_1} [MonoidWithZero α] {p q : α} (h₁ : q ≠ 0) (h₂ : p ∣ q) :
p ≠ 0
source
theorem isPrimal_zero {α : Type u_1} [MonoidWithZero α] :
IsPrimal 0
source
theorem IsPrimal.mul {α : Type u_2} [CancelCommMonoidWithZero α] {m n : α} (hm : IsPrimal m) (hn : IsPrimal n) :
IsPrimal (m * n)
source
theorem dvd_antisymm {α : Type u_1} [CancelCommMonoidWithZero α] {a b : α} [Subsingleton α ˣ] :
a ∣ b → b ∣ a → a = b
source
theorem dvd_antisymm' {α : Type u_1} [CancelCommMonoidWithZero α] {a b : α} [Subsingleton α ˣ] :
a ∣ b → b ∣ a → b = a
source
theorem Dvd.dvd.antisymm {α : Type u_1} [CancelCommMonoidWithZero α] {a b : α} [Subsingleton α ˣ] :
a ∣ b → b ∣ a → a = b

Alias of `dvd_antisymm`.

source
theorem Dvd.dvd.antisymm' {α : Type u_1} [CancelCommMonoidWithZero α] {a b : α} [Subsingleton α ˣ] :
a ∣ b → b ∣ a → b = a

Alias of `dvd_antisymm'`.

source
theorem eq_of_forall_dvd {α : Type u_1} [CancelCommMonoidWithZero α] {a b : α} [Subsingleton α ˣ] (h : ∀ (c : α), a ∣ c ↔ b ∣ c) :
a = b
source
theorem eq_of_forall_dvd' {α : Type u_1} [CancelCommMonoidWithZero α] {a b : α} [Subsingleton α ˣ] (h : ∀ (c : α), c ∣ a ↔ c ∣ b) :
a = b
source
theorem pow_dvd_pow_iff {α : Type u_1} [CancelCommMonoidWithZero α] {a : α} {m n : ℕ} (ha₀ : a ≠ 0) (ha : ¬IsUnit a) :
a ^ n ∣ a ^ m ↔ n ≤ m
source
@[simp]
theorem GroupWithZero.dvd_iff {α : Type u_1} [GroupWithZero α] {m n : α} :
m ∣ n ↔ m = 0 → n = 0

`∣` is not a useful definition if an inverse is available.