Structures · Lean core
RatCast
Type class for the canonical homomorphism Rat → K.
- Defined in
- Batteries.Classes.RatCast
- Shape
- One type argument · adds ratCast
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances16
- Real
- Rat
- Complex
- Quaternion
- WithVal
- HahnSeries
- QuadraticAlgebra
- ArchimedeanClass.FiniteElement
- CauSeq.Completion.Cauchy
- Subtype
- OrderDual
- ULift
- MulOpposite
- Lex
- AddOpposite
- Shrink
How is a type an instance?
Loading the hierarchy index…
Assumed by21
- MulOpposite.unop_ratCast
- HahnSeries.single_zero_ratCast
- Equiv.ratCast
- OrderDual.instRatCast
- Shrink.instRatCast
- Function.Injective.divisionRing
- MulOpposite.op_ratCast
- HahnSeries.instRatCast
- ULift.down_ratCast
- AddOpposite.unop_ratCast
- ofDual_ratCast
- Function.Injective.field
- AddOpposite.instRatCast
- MulOpposite.instRatCast
- toLex_ratCast
- toDual_ratCast
- Lex.instRatCast
- ULift.instRatCast
- AddOpposite.op_ratCast
- ofLex_ratCast
- ULift.up_ratCast
Ancestors0
No ancestors.