Mathlib Map

Structures · Lean core

Dvd

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

Defined in
Init.Prelude
Shape
One type argument · adds dvd

Extends0

Extends nothing: this is a root of the hierarchy.

Extended by1

Forgetful instances

Provided automatically by

Concrete types that are instances3

  • Int
  • Nat
  • PosNum

How is a type an instance?

Loading the hierarchy index…

Assumed by10

Ancestors0

No ancestors.