PUnit is a commutative ring

This file collects facts about algebraic structures on the one-element type, e.g. that it is a commutative ring.

instance PUnit.commRing : CommRing PUnit.{u_1 + 1}

Equations

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

instance PUnit.instIsCancelMulZero : IsCancelMulZero PUnit.{u_1 + 1}