Structures · Lean core
HPow
The notation typeclass for heterogeneous exponentiation.
This enables the notation a ^ b : γ where a : α, b : β.
- Defined in
- Init.Prelude
- Shape
- 3 explicit arguments · adds hPow
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances3
- Lean.Grind.Ring.OfSemiring.Q
- Aesop.Percent
- Fin
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.