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.{u_1 + 1}

Equations

• One or more equations did not get rendered due to their size.

instance PUnit.addCommGroup : AddCommGroup PUnit.{u_1 + 1}

Equations

• One or more equations did not get rendered due to their size.

instance PUnit.instOne_mathlib : One PUnit.{u_1 + 1}

Equations

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

instance PUnit.instZero_mathlib : Zero PUnit.{u_1 + 1}

Equations

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

instance PUnit.instMul_mathlib : Mul PUnit.{u_1 + 1}

Equations

• PUnit.instMul_mathlib = { mul := fun (x x : PUnit.{?u.1 + 1}) => PUnit.unit }

instance PUnit.instAdd_mathlib : Add PUnit.{u_1 + 1}

Equations

• PUnit.instAdd_mathlib = { add := fun (x x : PUnit.{?u.1 + 1}) => PUnit.unit }

instance PUnit.instDiv_mathlib : Div PUnit.{u_1 + 1}

Equations

• PUnit.instDiv_mathlib = { div := fun (x x : PUnit.{?u.1 + 1}) => PUnit.unit }

instance PUnit.instSub_mathlib : Sub PUnit.{u_1 + 1}

Equations

• PUnit.instSub_mathlib = { sub := fun (x x : PUnit.{?u.1 + 1}) => PUnit.unit }

instance PUnit.instInv_mathlib : Inv PUnit.{u_1 + 1}

Equations

• PUnit.instInv_mathlib = { inv := fun (x : PUnit.{?u.1 + 1}) => PUnit.unit }

instance PUnit.instNeg_mathlib : Neg PUnit.{u_1 + 1}

Equations

• PUnit.instNeg_mathlib = { neg := fun (x : PUnit.{?u.1 + 1}) => PUnit.unit }

@[simp]

theorem PUnit.one_eq : 1 = unit

@[simp]

theorem PUnit.zero_eq : 0 = unit

theorem PUnit.mul_eq (x y : PUnit.{u_1 + 1}) : x * y = unit

theorem PUnit.add_eq (x y : PUnit.{u_1 + 1}) : x + y = unit

@[simp]

theorem PUnit.div_eq (x y : PUnit.{u_1 + 1}) : x / y = unit

@[simp]

theorem PUnit.sub_eq (x y : PUnit.{u_1 + 1}) : x - y = unit

@[simp]

theorem PUnit.inv_eq (x : PUnit.{u_1 + 1}) : x⁻¹ = unit

@[simp]

theorem PUnit.neg_eq (x : PUnit.{u_1 + 1}) : -x = unit