Documentation

Batteries.Classes.RatCast

source
class RatCast (K : Type u) :
Type u

Type class for the canonical homomorphism Rat → K.

  • ratCast : Rat → K

    The canonical homomorphism Rat → K.

Instances
    source
    instance instRatCastRat :
    RatCast Rat
    Equations
      source
      @[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
        Instances For
          source
          instance instCoeTailRatOfRatCast {K : Type u_1} [RatCast K] :
          CoeTail Rat K
          Equations
            source
            instance instCoeHTCTRatOfRatCast {K : Type u_1} [RatCast K] :
            CoeHTCT Rat K
            Equations