Divisibility in groups with zero. #
Lemmas about divisibility in groups and monoids with zero.
@[simp]
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
mul_dvd_mul_iff_left
{α : Type u_1}
[inst : CancelMonoidWithZero α]
{a : α}
{b : α}
{c : α}
(ha : a ≠ 0)
:
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)
:
Given two elements a
, b
of a commutative CancelMonoidWithZero
and a nonzero
element c
, a*c
divides b*c
iff a
divides b
.
DvdNotUnit a b
expresses that a
divides b
"strictly", i.e. that b
divided by a
is not a unit.
theorem
dvdNotUnit_of_dvd_of_not_dvd
{α : Type u_1}
[inst : CommMonoidWithZero α]
{a : α}
{b : α}
(hd : a ∣ b)
(hnd : ¬b ∣ a)
:
DvdNotUnit a b
theorem
ne_zero_of_dvd_ne_zero
{α : Type u_1}
[inst : MonoidWithZero α]
{p : α}
{q : α}
(h₁ : q ≠ 0)
(h₂ : p ∣ q)
:
p ≠ 0