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.cancelCommMonoidWithZero : CancelCommMonoidWithZero PUnit.{u_1 + 1}

Equations

• PUnit.cancelCommMonoidWithZero = { toCommMonoidWithZero := CommSemiring.toCommMonoidWithZero, toIsLeftCancelMulZero := PUnit.cancelCommMonoidWithZero._proof_17 }