class RatCast (K : Type u) : Type u

Type class for the canonical homomorphism Rat → K.

• ratCast : Rat → K

  The canonical homomorphism Rat → K.

instance instRatCastRat : RatCast Rat

Equations

• instRatCastRat = { ratCast := fun (n : Rat) => n }

@[match_pattern, reducible]

def Rat.cast {K : Type u} [RatCast K] : Rat → K

Canonical homomorphism from Rat to a division ring K. This is just the bare function in order to aid in creating instances of DivisionRing.

Equations

• Rat.cast = RatCast.ratCast

instance instCoeTailRat {K : Type u_1} [RatCast K] : CoeTail Rat K

Equations

• instCoeTailRat = { coe := Rat.cast }

instance instCoeHTCTRat {K : Type u_1} [RatCast K] : CoeHTCT Rat K

Equations

• instCoeHTCTRat = { coe := Rat.cast }