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

Equations

• PUnit.commGroup = CommGroup.mk PUnit.commGroup.proof_11

instance PUnit.addCommGroup : AddCommGroup PUnit

Equations

• PUnit.addCommGroup = AddCommGroup.mk PUnit.addCommGroup.proof_11

instance PUnit.instOne : One PUnit

Equations

• PUnit.instOne = { one := PUnit.unit }

instance PUnit.instZero : Zero PUnit

Equations

• PUnit.instZero = { zero := PUnit.unit }

instance PUnit.instMul_mathlib : Mul PUnit

Equations

• PUnit.instMul_mathlib = { mul := fun (x x : PUnit) => PUnit.unit }

instance PUnit.instAdd_mathlib : Add PUnit

Equations

• PUnit.instAdd_mathlib = { add := fun (x x : PUnit) => PUnit.unit }

instance PUnit.instDiv_mathlib : Div PUnit

Equations

• PUnit.instDiv_mathlib = { div := fun (x x : PUnit) => PUnit.unit }

instance PUnit.instSub_mathlib : Sub PUnit

Equations

• PUnit.instSub_mathlib = { sub := fun (x x : PUnit) => PUnit.unit }

instance PUnit.instInv : Inv PUnit

Equations

• PUnit.instInv = { inv := fun (x : PUnit) => PUnit.unit }

instance PUnit.instNeg : Neg PUnit

Equations

• PUnit.instNeg = { neg := fun (x : PUnit) => PUnit.unit }

@[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