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

Equations
  • ULift.instNNRatCast = { nnratCast := fun (q : ℚ≥0) => { down := q } }
instance ULift.instRatCast {α : Type u} [RatCast α] :
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
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • ULift.semifield = let __src := ULift.divisionSemiring; let __src_1 := ULift.commGroupWithZero; Semifield.mk DivisionSemiring.zpow DivisionSemiring.nnqsmul
Equations
  • One or more equations did not get rendered due to their size.
instance ULift.field {α : Type u} [Field α] :
Equations
  • ULift.field = let __src := ULift.semifield; let __src_1 := ULift.divisionRing; Field.mk Semifield.zpow Semifield.nnqsmul DivisionRing.qsmul