Documentation

Std.Classes.Dvd

class Dvd (α : Type u_1) :
Type u_1

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

  • dvd : ααProp

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

Instances

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

    Equations
    Instances For