Documentation

Mathlib.Algebra.GroupWithZero.ULift

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

source
instance ULift.mulZeroOneClass {α : Type u} [MulZeroOneClass α] :
MulZeroOneClass (ULift.{u_1, u} α)
Equations
    source
    instance ULift.monoidWithZero {α : Type u} [MonoidWithZero α] :
    MonoidWithZero (ULift.{u_1, u} α)
    Equations
      source
      instance ULift.commMonoidWithZero {α : Type u} [CommMonoidWithZero α] :
      CommMonoidWithZero (ULift.{u_1, u} α)
      Equations
        source
        instance ULift.groupWithZero {α : Type u} [GroupWithZero α] :
        GroupWithZero (ULift.{u_1, u} α)
        Equations
          source
          instance ULift.commGroupWithZero {α : Type u} [CommGroupWithZero α] :
          CommGroupWithZero (ULift.{u_1, u} α)
          Equations