Divisibility
This file defines the basics of the divisibility relation in the context of (comm_) monoids
(_with_zero).
Main definitions
monoid.has_dvd
Implementation notes
The divisibility relation is defined for all monoids, and as such, depends on the order of
multiplication if the monoid is not commutative. There are two possible conventions for
divisibility in the noncommutative context, and this relation follows the convention for ordinals,
so a | b is defined as ∃ c, b = a * c.
Tags
divisibility, divides
There are two possible conventions for divisibility, which coincide in a comm_monoid.
This matches the convention for ordinals.
Given an element a of a commutative monoid with zero, there exists another element whose
product with zero equals a iff a equals zero.
Given two elements b, c of a cancel_monoid_with_zero and a nonzero element a,
a*b divides a*c iff b divides c.
Given two elements a, b of a commutative cancel_monoid_with_zero and a nonzero
element c, a*c divides b*c iff a divides b.
Units in various monoids
In a commutative monoid, an element a divides an element b iff a divides all left
associates of b.
In a commutative monoid, an element a divides an element b iff all
left associates of a divide b.
Units of a monoid divide any element of the monoid.
In a commutative monoid, an element a divides an element b iff a divides all left
associates of b.
In a commutative monoid, an element a divides an element b iff all
left associates of a divide b.