Instances on PUnit

This file collects facts about ordered algebraic structures on the one-element type.

instance PUnit.canonicallyOrderedAdd : CanonicallyOrderedAdd PUnit.{u_1 + 1}

instance PUnit.linearOrderedCancelAddCommMonoid : LinearOrderedCancelAddCommMonoid PUnit.{u_1 + 1}

Equations

• PUnit.linearOrderedCancelAddCommMonoid = LinearOrderedCancelAddCommMonoid.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯

instance PUnit.instLinearOrderedAddCommMonoidWithTop : LinearOrderedAddCommMonoidWithTop PUnit.{u_1 + 1}

Equations

• PUnit.instLinearOrderedAddCommMonoidWithTop = LinearOrderedAddCommMonoidWithTop.mk PUnit.instLinearOrderedAddCommMonoidWithTop.proof_2