Divisibility in groups with zero.

Lemmas about divisibility in groups and monoids with zero.

theorem eq_zero_of_zero_dvd {α : Type u_1} [SemigroupWithZero α] {a : α} (h : Dvd.dvd 0 a) : Eq a 0

theorem zero_dvd_iff {α : Type u_1} [SemigroupWithZero α] {a : α} : Iff (Dvd.dvd 0 a) (Eq 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.

theorem dvd_zero {α : Type u_1} [SemigroupWithZero α] (a : α) : Dvd.dvd a 0

theorem mul_dvd_mul_iff_left {α : Type u_1} [CancelMonoidWithZero α] {a b c : α} (ha : Ne a 0) : Iff (Dvd.dvd (HMul.hMul a b) (HMul.hMul a c)) (Dvd.dvd 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} [CancelCommMonoidWithZero α] {a b c : α} (hc : Ne c 0) : Iff (Dvd.dvd (HMul.hMul a c) (HMul.hMul b c)) (Dvd.dvd 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} [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

• Eq (DvdNotUnit a b) (And (Ne a 0) (Exists fun (x : α) => And (Not (IsUnit x)) (Eq b (HMul.hMul a x))))

theorem dvdNotUnit_of_dvd_of_not_dvd {α : Type u_1} [CommMonoidWithZero α] {a b : α} (hd : Dvd.dvd a b) (hnd : Not (Dvd.dvd b a)) : DvdNotUnit a b

theorem isRelPrime_zero_left {α : Type u_1} [CommMonoidWithZero α] {x : α} : Iff (IsRelPrime 0 x) (IsUnit x)

theorem isRelPrime_zero_right {α : Type u_1} [CommMonoidWithZero α] {x : α} : Iff (IsRelPrime x 0) (IsUnit x)

theorem not_isRelPrime_zero_zero {α : Type u_1} [CommMonoidWithZero α] [Nontrivial α] : Not (IsRelPrime 0 0)

theorem IsRelPrime.ne_zero_or_ne_zero {α : Type u_1} [CommMonoidWithZero α] {x y : α} [Nontrivial α] (h : IsRelPrime x y) : Or (Ne x 0) (Ne y 0)

theorem isRelPrime_of_no_nonunits_factors {α : Type u_1} [MonoidWithZero α] {x y : α} (nonzero : Not (And (Eq x 0) (Eq y 0))) (H : ∀ (z : α), Not (IsUnit z) → Ne z 0 → Dvd.dvd z x → Not (Dvd.dvd z y)) : IsRelPrime x y

theorem dvd_and_not_dvd_iff {α : Type u_1} [CancelCommMonoidWithZero α] {x y : α} : Iff (And (Dvd.dvd x y) (Not (Dvd.dvd y x))) (DvdNotUnit x y)

theorem ne_zero_of_dvd_ne_zero {α : Type u_1} [MonoidWithZero α] {p q : α} (h₁ : Ne q 0) (h₂ : Dvd.dvd p q) : Ne p 0

theorem isPrimal_zero {α : Type u_1} [MonoidWithZero α] : IsPrimal 0

theorem IsPrimal.mul {α : Type u_2} [CancelCommMonoidWithZero α] {m n : α} (hm : IsPrimal m) (hn : IsPrimal n) : IsPrimal (HMul.hMul m n)

theorem dvd_antisymm {α : Type u_1} [CancelCommMonoidWithZero α] {a b : α} [Subsingleton (Units α)] : Dvd.dvd a b → Dvd.dvd b a → Eq a b

theorem dvd_antisymm' {α : Type u_1} [CancelCommMonoidWithZero α] {a b : α} [Subsingleton (Units α)] : Dvd.dvd a b → Dvd.dvd b a → Eq b a

theorem Dvd.dvd.antisymm {α : Type u_1} [CancelCommMonoidWithZero α] {a b : α} [Subsingleton (Units α)] : dvd a b → dvd b a → Eq a b

Alias of dvd_antisymm.

theorem Dvd.dvd.antisymm' {α : Type u_1} [CancelCommMonoidWithZero α] {a b : α} [Subsingleton (Units α)] : dvd a b → dvd b a → Eq b a

Alias of dvd_antisymm'.

theorem eq_of_forall_dvd {α : Type u_1} [CancelCommMonoidWithZero α] {a b : α} [Subsingleton (Units α)] (h : ∀ (c : α), Iff (Dvd.dvd a c) (Dvd.dvd b c)) : Eq a b

theorem eq_of_forall_dvd' {α : Type u_1} [CancelCommMonoidWithZero α] {a b : α} [Subsingleton (Units α)] (h : ∀ (c : α), Iff (Dvd.dvd c a) (Dvd.dvd c b)) : Eq a b

theorem pow_dvd_pow_iff {α : Type u_1} [CancelCommMonoidWithZero α] {a : α} {m n : Nat} (ha₀ : Ne a 0) (ha : Not (IsUnit a)) : Iff (Dvd.dvd (HPow.hPow a n) (HPow.hPow a m)) (LE.le n m)

theorem GroupWithZero.dvd_iff {α : Type u_1} [GroupWithZero α] {m n : α} : Iff (Dvd.dvd m n) (Eq m 0 → Eq n 0)

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