Instances on PUnit

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

instance PUnit.canonicallyOrderedAddCommMonoid : CanonicallyOrderedAddCommMonoid PUnit.{u_1 + 1}

Equations

• PUnit.canonicallyOrderedAddCommMonoid = CanonicallyOrderedAddCommMonoid.mk @PUnit.canonicallyOrderedAddCommMonoid.proof_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_1