Documentation

Mathlib.Algebra.Ring.PUnit

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.

source
instance PUnit.commRing :
CommRing PUnit.{u_1 + 1}
Equations
source
instance PUnit.cancelCommMonoidWithZero :
CancelCommMonoidWithZero PUnit.{u_1 + 1}
Equations