ULift instances for groups and monoids with zero

This file defines instances for group and monoid with zero and related structures on ULift types.

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

instance ULift.mulZeroOneClass {α : Type u} [MulZeroOneClass α] : MulZeroOneClass (ULift.{u_1, u} α)

Equations

• ULift.mulZeroOneClass = Function.Injective.mulZeroOneClass ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯

instance ULift.monoidWithZero {α : Type u} [MonoidWithZero α] : MonoidWithZero (ULift.{u_1, u} α)

Equations

• ULift.monoidWithZero = Function.Injective.monoidWithZero ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯ ⋯

instance ULift.commMonoidWithZero {α : Type u} [CommMonoidWithZero α] : CommMonoidWithZero (ULift.{u_1, u} α)

Equations

• ULift.commMonoidWithZero = Function.Injective.commMonoidWithZero ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯ ⋯

instance ULift.groupWithZero {α : Type u} [GroupWithZero α] : GroupWithZero (ULift.{u_1, u} α)

Equations

• ULift.groupWithZero = Function.Injective.groupWithZero ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance ULift.commGroupWithZero {α : Type u} [CommGroupWithZero α] : CommGroupWithZero (ULift.{u_1, u} α)

Equations

• ULift.commGroupWithZero = Function.Injective.commGroupWithZero ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯