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.)

instance ULift.instNNRatCast {α : Type u} [NNRatCast α] : NNRatCast (ULift.{u_1, u} α)

Equations

• ULift.instNNRatCast = { nnratCast := fun (q : ℚ≥0) => { down := ↑q } }

instance ULift.instRatCast {α : Type u} [RatCast α] : RatCast (ULift.{u_1, u} α)

Equations

• ULift.instRatCast = { ratCast := fun (q : ℚ) => { down := ↑q } }

@[simp]

theorem ULift.up_nnratCast {α : Type u} [NNRatCast α] (q : ℚ≥0) : { down := ↑q } = ↑q

@[simp]

theorem ULift.down_nnratCast {α : Type u} [NNRatCast α] (q : ℚ≥0) : (↑q).down = ↑q

@[simp]

theorem ULift.up_ratCast {α : Type u} [RatCast α] (q : ℚ) : { down := ↑q } = ↑q

@[simp]

theorem ULift.down_ratCast {α : Type u} [RatCast α] (q : ℚ) : (↑q).down = ↑q

instance ULift.divisionSemiring {α : Type u} [DivisionSemiring α] : DivisionSemiring (ULift.{u_1, u} α)

Equations

• ULift.divisionSemiring = Function.Injective.divisionSemiring ULift.down ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance ULift.semifield {α : Type u} [Semifield α] : Semifield (ULift.{u_1, u} α)

Equations

• ULift.semifield = let __src := ULift.divisionSemiring; let __src_1 := ULift.commGroupWithZero; Semifield.mk ⋯ DivisionSemiring.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ DivisionSemiring.nnqsmul ⋯

instance ULift.divisionRing {α : Type u} [DivisionRing α] : DivisionRing (ULift.{u_1, u} α)

Equations

• ULift.divisionRing = Function.Injective.divisionRing ULift.down ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance ULift.field {α : Type u} [Field α] : Field (ULift.{u_1, u} α)

Equations

• ULift.field = let __src := ULift.semifield; let __src_1 := ULift.divisionRing; Field.mk ⋯ Semifield.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ Semifield.nnqsmul ⋯ ⋯ DivisionRing.qsmul ⋯