Theorems · Definition · number theory
NNRatCast.nnratCast
{K : Type u_1} → [self : NNRatCast K] → ℚ≥0 → KThe canonical homomorphism ℚ≥0 → K.
Do not use directly. Use the coercion instead.
- Defined in
- Mathlib.Data.Rat.Init
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 40 from the axioms · uses propext, Quot.sound
- Assumes
- NNRatCast
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by3
Results whose statement or proof uses this declaration.
- NNRat.castproof · cited by 235
- QuadraticAlgebra.im_nnratCaststatement and proof · cited by 0
- QuadraticAlgebra.re_nnratCaststatement and proof · cited by 0