mathlib3 documentation

algebra.ring.ulift

ulift instances for ring #

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

This file defines instances for ring, semiring and related structures on ulift types.

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

We also provide ulift.ring_equiv : ulift R ≃+* R.

@[protected, instance]
Equations
@[protected, instance]
def ulift.distrib {α : Type u} [distrib α] :
Equations

The ring equivalence between ulift α and α.

Equations