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.

def «term_∣_» : Lean.TrailingParserDescr

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

Equations

• «term_∣_» = Lean.ParserDescr.trailingNode `term_∣_ 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∣ ") (Lean.ParserDescr.cat `term 51))