Mathlib Map

Structures · Lean core

HMod

The notation typeclass for heterogeneous modulo / remainder. This enables the notation a % b : γ where a : α, b : β.

Defined in
Init.Prelude
Shape
3 explicit arguments · adds hMod
Open in Mathlib docs

Extends0

Extends nothing: this is a root of the hierarchy.

Extended by1

Forgetful instances

Provided automatically by

Concrete types that are instances5

  • UInt64
  • UInt8
  • UInt16
  • UInt32
  • USize

How is a type an instance?

Loading the hierarchy index…

Assumed by0

No theorem or definition in Mathlib takes this class as a hypothesis.

Ancestors0

No ancestors.