Documentation

Mathlib.Algebra.Group.PUnit

`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

instance PUnit.addCommGroup :

AddCommGroup PUnit.{u_1 + 1}

Equations

instance PUnit.instOne_mathlib :

One PUnit.{u_1 + 1}

Equations

instance PUnit.instZero_mathlib :

Zero PUnit.{u_1 + 1}

Equations

instance PUnit.instMul_mathlib :

Mul PUnit.{u_1 + 1}

Equations

instance PUnit.instAdd_mathlib :

Add PUnit.{u_1 + 1}

Equations

instance PUnit.instDiv_mathlib :

Div PUnit.{u_1 + 1}

Equations

instance PUnit.instSub_mathlib :

Sub PUnit.{u_1 + 1}

Equations

instance PUnit.instInv_mathlib :

Inv PUnit.{u_1 + 1}

Equations

instance PUnit.instNeg_mathlib :

Neg PUnit.{u_1 + 1}

Equations

@[simp]

theorem PUnit.one_eq :

@[simp]

theorem PUnit.zero_eq :

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}) :

@[simp]

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