Structures · Data types
NNRatCast
Typeclass for the canonical homomorphism ℚ≥0 → K.
This should be considered as a notation typeclass. The sole purpose of this typeclass is to be
extended by DivisionSemiring.
- Defined in
- Mathlib.Data.Rat.Init
- Shape
- One type argument · adds nnratCast
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Forgetful instances
Every NNRatCast is also a
Concrete types that are instances17
- Real
- Rat
- Complex
- NNReal
- ENNReal
- NNRat
- Quaternion
- WithVal
- HahnSeries
- QuadraticAlgebra
- CauSeq.Completion.Cauchy
- Subtype
- OrderDual
- ULift
- MulOpposite
- AddOpposite
- Shrink
How is a type an instance?
Loading the hierarchy index…
Assumed by26
- NNRat.cast
- NNRatCast.nnratCast
- NNRatCast.toOfScientific_def
- NNRat.cast_ofScientific
- MulOpposite.unop_nnratCast
- AddOpposite.op_nnratCast
- MulOpposite.instNNRatCast
- Function.Injective.divisionRing
- NNRatCast.toOfScientific
- NNRatCast.ofScientific_eq_ite
- HahnSeries.single_zero_nnratCast
- AddOpposite.unop_nnratCast
- ULift.instNNRatCast
- Equiv.nnratCast
- NNRatCast.toCoeHTCT
- MulOpposite.op_nnratCast
- Function.Injective.semifield
- AddOpposite.instNNRatCast
- Function.Injective.field
- Shrink.instNNRatCast
- ULift.up_nnratCast
- ULift.down_nnratCast
- HahnSeries.instNNRatCast
- NNRatCast.toCoeTail
- OrderDual.instNNRatCast
- Function.Injective.divisionSemiring