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

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

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

Equations

• PUnit.instLinearOrderedAddCommMonoidWithTop = LinearOrderedAddCommMonoidWithTop.mk PUnit.instLinearOrderedAddCommMonoidWithTop.proof_1