THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines the basics of the divisibility relation in the context of
Main definitions #
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,
a | b is defined as
∃ c, b = a * c.
There are two possible conventions for divisibility, which coincide in a
This matches the convention for ordinals.