mathlib3 documentation

algebra.field.ulift

Field instances for ulift #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

@[protected, instance]
Equations
@[simp, norm_cast]
theorem ulift.up_rat_cast {α : Type u} [has_rat_cast α] (q : ) :
{down := q} = q
@[simp, norm_cast]
theorem ulift.down_rat_cast {α : Type u} [has_rat_cast α] (q : ) :
@[protected, instance]
Equations
@[protected, instance]
Equations