ink

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.

ink

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))