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.

@[implicit_reducible]

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

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