# Documentation

Std.Classes.Dvd

class Dvd (α : Type u_1) :
Type u_1
• Divisibility. a ∣ b (typed as \|) means that there is some c such that b = a * c.

dvd : ααProp

Notation typeclass for the ∣ operation (typed as \|), which represents divisibility.

Instances

Divisibility. a ∣ b (typed as \|) means that there is some c such that b = a * c.

Equations