Divisibility in groups with zero. #

Lemmas about divisibility in groups and monoids with zero.

theorem eq_zero_of_zero_dvd {α : Type u_1} [inst : SemigroupWithZero α] {a : α} (h : 0 ∣ a) :

a = 0

@[simp]

theorem zero_dvd_iff {α : Type u_1} [inst : 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.

@[simp]

theorem dvd_zero {α : Type u_1} [inst : SemigroupWithZero α] (a : α) :

a ∣ 0

theorem mul_dvd_mul_iff_left {α : Type u_1} [inst : 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.

theorem mul_dvd_mul_iff_right {α : Type u_1} [inst : 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.

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

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

Equations

theorem dvdNotUnit_of_dvd_of_not_dvd {α : Type u_1} [inst : CommMonoidWithZero α] {a : α} {b : α} (hd : a ∣ b) (hnd : ¬b ∣ a) :

theorem dvd_and_not_dvd_iff {α : Type u_1} [inst : CancelCommMonoidWithZero α] {x : α} {y : α} :

theorem ne_zero_of_dvd_ne_zero {α : Type u_1} [inst : MonoidWithZero α] {p : α} {q : α} (h₁ : q ≠ 0) (h₂ : p ∣ q) :

p ≠ 0