class RatCast (K : Type u) : Type u

Type class for the canonical homomorphism Rat → K.

• ratCast : Rat → K

  The canonical homomorphism Rat → K.

@[implicit_reducible]

instance instRatCastRat : RatCast Rat

Equations

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

@[reducible, match_pattern]

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

@[implicit_reducible]

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

Equations

• instCoeTailRatOfRatCast = { coe := Rat.cast }

@[implicit_reducible]

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

Equations

• instCoeHTCTRatOfRatCast = { coe := Rat.cast }