Documentation

Mathlib.Algebra.Field.ULift

Field instances for ULift #

This file defines instances for fields, semifields, and related structures on ULift types.

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

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