Std.Classes.Dvd
source
Divisibility. a ∣ b (typed as \|) means that there is some c such that b = a * c.
a ∣ b
\|
c
b = a * c
Notation typeclass for the ∣ operation (typed as \|), which represents divisibility.
∣