Divisibility in groups with zero. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
Lemmas about divisibility in groups and monoids with zero.
Given an element
a of a commutative semigroup with zero, there exists another element whose
product with zero equals
a equals zero.
Given two elements
b of a commutative
cancel_monoid_with_zero and a nonzero
dvd_not_unit a b expresses that
b "strictly", i.e. that
b divided by
is not a unit.