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

@[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.field {α : Type u} [Field α] :