Documentation

Std.Classes.RatCast

class RatCast (K : Type u) :
  • ratCast : RatK

    The canonical homomorphism Rat → K.

Type class for the canonical homomorphism Rat → K.

Instances
    Equations
    @[match_pattern, reducible]
    def Rat.cast {K : Type u} [RatCast K] :
    RatK

    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
    Instances For
      instance instCoeTailRat {K : Type u_1} [RatCast K] :
      Equations
      • instCoeTailRat = { coe := Rat.cast }
      instance instCoeHTCTRat {K : Type u_1} [RatCast K] :
      Equations
      • instCoeHTCTRat = { coe := Rat.cast }