ULift instances for ring

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

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

We also provide ULift.ringEquiv : ULift R ≃+* R.

instance ULift.mulZeroClass {M₀ : Type u_1} [MulZeroClass M₀] : MulZeroClass (ULift.{u_2, u_1} M₀)

Equations

• ULift.mulZeroClass = { toMul := ULift.mul, toZero := ULift.zero, zero_mul := ⋯, mul_zero := ⋯ }

instance ULift.distrib {R : Type u} [Distrib R] : Distrib (ULift.{u_1, u} R)

Equations

• ULift.distrib = { toMul := ULift.mul, toAdd := ULift.add, left_distrib := ⋯, right_distrib := ⋯ }

instance ULift.instNatCast {R : Type u} [NatCast R] : NatCast (ULift.{u_1, u} R)

Equations

• ULift.instNatCast = { natCast := fun (x : ℕ) => { down := ↑x } }

instance ULift.instIntCast {R : Type u} [IntCast R] : IntCast (ULift.{u_1, u} R)

Equations

• ULift.instIntCast = { intCast := fun (x : ℤ) => { down := ↑x } }

@[simp]

theorem ULift.up_natCast {R : Type u} [NatCast R] (n : ℕ) : { down := ↑n } = ↑n

@[simp]

theorem ULift.up_ofNat {R : Type u} [NatCast R] (n : ℕ) [n.AtLeastTwo] : { down := OfNat.ofNat n } = OfNat.ofNat n

@[simp]

theorem ULift.up_intCast {R : Type u} [IntCast R] (n : ℤ) : { down := ↑n } = ↑n

@[simp]

theorem ULift.down_natCast {R : Type u} [NatCast R] (n : ℕ) : (↑n).down = ↑n

@[simp]

theorem ULift.down_ofNat {R : Type u} [NatCast R] (n : ℕ) [n.AtLeastTwo] : (OfNat.ofNat n).down = OfNat.ofNat n

@[simp]

theorem ULift.down_intCast {R : Type u} [IntCast R] (n : ℤ) : (↑n).down = ↑n

instance ULift.addMonoidWithOne {R : Type u} [AddMonoidWithOne R] : AddMonoidWithOne (ULift.{u_1, u} R)

Equations

• ULift.addMonoidWithOne = { toNatCast := ULift.instNatCast, toAddMonoid := ULift.addMonoid, toOne := ULift.one, natCast_zero := ⋯, natCast_succ := ⋯ }

instance ULift.addCommMonoidWithOne {R : Type u} [AddCommMonoidWithOne R] : AddCommMonoidWithOne (ULift.{u_1, u} R)

Equations

• ULift.addCommMonoidWithOne = { toAddMonoidWithOne := ULift.addMonoidWithOne, add_comm := ⋯ }

instance ULift.addGroupWithOne {R : Type u} [AddGroupWithOne R] : AddGroupWithOne (ULift.{u_1, u} R)

Equations

• One or more equations did not get rendered due to their size.

instance ULift.addCommGroupWithOne {R : Type u} [AddCommGroupWithOne R] : AddCommGroupWithOne (ULift.{u_1, u} R)

Equations

• One or more equations did not get rendered due to their size.

instance ULift.nonUnitalNonAssocSemiring {R : Type u} [NonUnitalNonAssocSemiring R] : NonUnitalNonAssocSemiring (ULift.{u_1, u} R)

Equations

• ULift.nonUnitalNonAssocSemiring = { toAddCommMonoid := ULift.addCommMonoid, toMul := ULift.distrib.toMul, left_distrib := ⋯, right_distrib := ⋯, zero_mul := ⋯, mul_zero := ⋯ }

instance ULift.nonAssocSemiring {R : Type u} [NonAssocSemiring R] : NonAssocSemiring (ULift.{u_1, u} R)

Equations

• One or more equations did not get rendered due to their size.

instance ULift.nonUnitalSemiring {R : Type u} [NonUnitalSemiring R] : NonUnitalSemiring (ULift.{u_1, u} R)

Equations

• ULift.nonUnitalSemiring = { toNonUnitalNonAssocSemiring := ULift.nonUnitalNonAssocSemiring, mul_assoc := ⋯ }

instance ULift.semiring {R : Type u} [Semiring R] : Semiring (ULift.{u_1, u} R)

Equations

• One or more equations did not get rendered due to their size.

def ULift.ringEquiv {R : Type u} [NonUnitalNonAssocSemiring R] : ULift.{u_1, u} R ≃+* R

The ring equivalence between ULift R and R.

Equations

• ULift.ringEquiv = { toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }

instance ULift.nonUnitalCommSemiring {R : Type u} [NonUnitalCommSemiring R] : NonUnitalCommSemiring (ULift.{u_1, u} R)

Equations

• ULift.nonUnitalCommSemiring = { toNonUnitalSemiring := ULift.nonUnitalSemiring, mul_comm := ⋯ }

instance ULift.commSemiring {R : Type u} [CommSemiring R] : CommSemiring (ULift.{u_1, u} R)

Equations

• ULift.commSemiring = { toSemiring := ULift.semiring, mul_comm := ⋯ }

instance ULift.nonUnitalNonAssocRing {R : Type u} [NonUnitalNonAssocRing R] : NonUnitalNonAssocRing (ULift.{u_1, u} R)

Equations

• ULift.nonUnitalNonAssocRing = { toAddCommGroup := ULift.addCommGroup, toMul := ULift.nonUnitalNonAssocSemiring.toMul, left_distrib := ⋯, right_distrib := ⋯, zero_mul := ⋯, mul_zero := ⋯ }

instance ULift.nonUnitalRing {R : Type u} [NonUnitalRing R] : NonUnitalRing (ULift.{u_1, u} R)

Equations

• ULift.nonUnitalRing = { toNonUnitalNonAssocRing := ULift.nonUnitalNonAssocRing, mul_assoc := ⋯ }

instance ULift.nonAssocRing {R : Type u} [NonAssocRing R] : NonAssocRing (ULift.{u_1, u} R)

Equations

• One or more equations did not get rendered due to their size.

instance ULift.ring {R : Type u} [Ring R] : Ring (ULift.{u_1, u} R)

Equations

• One or more equations did not get rendered due to their size.

instance ULift.nonUnitalCommRing {R : Type u} [NonUnitalCommRing R] : NonUnitalCommRing (ULift.{u_1, u} R)

Equations

• ULift.nonUnitalCommRing = { toNonUnitalRing := ULift.nonUnitalRing, mul_comm := ⋯ }

instance ULift.commRing {R : Type u} [CommRing R] : CommRing (ULift.{u_1, u} R)

Equations

• ULift.commRing = { toRing := ULift.ring, mul_comm := ⋯ }