PUnit is a commutative group

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

instance PUnit.commGroup : CommGroup PUnit

instance PUnit.addCommGroup : AddCommGroup PUnit

instance PUnit.instOne_mathlib : One PUnit

instance PUnit.instZero_mathlib : Zero PUnit

instance PUnit.instMul_mathlib : Mul PUnit

instance PUnit.instAdd_mathlib : Add PUnit

instance PUnit.instDiv_mathlib : Div PUnit

instance PUnit.instSub_mathlib : Sub PUnit

instance PUnit.instInv_mathlib : Inv PUnit

instance PUnit.instNeg_mathlib : Neg PUnit

@[simp]

theorem PUnit.one_eq : 1 = unit

@[simp]

theorem PUnit.zero_eq : 0 = unit

theorem PUnit.mul_eq (x y : PUnit) : x * y = unit

theorem PUnit.add_eq (x y : PUnit) : x + y = unit

@[simp]

theorem PUnit.div_eq (x y : PUnit) : x / y = unit

@[simp]

theorem PUnit.sub_eq (x y : PUnit) : x - y = unit

@[simp]

theorem PUnit.inv_eq (x : PUnit) : x⁻¹ = unit

@[simp]

theorem PUnit.neg_eq (x : PUnit) : -x = unit