class Dvd (α : Type u_1) : Type u_1

• dvd : α → α → Prop

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

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

def «term_∣_» : Lean.TrailingParserDescr

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