Structures · Lean core
HDiv
The notation typeclass for heterogeneous division.
This enables the notation a / b : γ where a : α, b : β.
- Defined in
- Init.Prelude
- Shape
- 3 explicit arguments · adds hDiv
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances2
- System.FilePath
- Aesop.Nanos
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.