Documentation

Mathlib.Algebra.Field.ULift

Field instances for ULift #

This file defines instances for field, semifield and related structures on ULift types.

(Recall ULift α is just a "copy" of a type α in a higher universe.)

source
instance ULift.instNNRatCast {α : Type u} [NNRatCast α] :
NNRatCast (ULift.{u_1, u} α)
Equations
    source
    instance ULift.instRatCast {α : Type u} [RatCast α] :
    RatCast (ULift.{u_1, u} α)
    Equations
      source
      @[simp]
      theorem ULift.up_nnratCast {α : Type u} [NNRatCast α] (q : ℚ≥0) :
      { down := ↑q } = ↑q
      source
      @[simp]
      theorem ULift.down_nnratCast {α : Type u} [NNRatCast α] (q : ℚ≥0) :
      (↑q).down = ↑q
      source
      @[simp]
      theorem ULift.up_ratCast {α : Type u} [RatCast α] (q : ℚ) :
      { down := ↑q } = ↑q
      source
      @[simp]
      theorem ULift.down_ratCast {α : Type u} [RatCast α] (q : ℚ) :
      (↑q).down = ↑q
      source
      instance ULift.divisionSemiring {α : Type u} [DivisionSemiring α] :
      DivisionSemiring (ULift.{u_1, u} α)
      Equations
        source
        instance ULift.semifield {α : Type u} [Semifield α] :
        Semifield (ULift.{u_1, u} α)
        Equations
          source
          instance ULift.divisionRing {α : Type u} [DivisionRing α] :
          DivisionRing (ULift.{u_1, u} α)
          Equations
            source
            instance ULift.field {α : Type u} [Field α] :
            Field (ULift.{u_1, u} α)
            Equations