Instances on PUnit

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

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

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

Equations

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

instance PUnit.instOne : One PUnit.{1}

Equations

• PUnit.instOne = { one := () }

instance PUnit.instZero : Zero PUnit.{1}

Equations

• PUnit.instZero = { zero := () }

instance PUnit.instMul_mathlib : Mul PUnit.{1}

Equations

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

instance PUnit.instAdd_mathlib : Add PUnit.{1}

Equations

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

instance PUnit.instDiv_mathlib : Div PUnit.{1}

Equations

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

instance PUnit.instSub_mathlib : Sub PUnit.{1}

Equations

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

instance PUnit.instInv : Inv PUnit.{1}

Equations

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

instance PUnit.instNeg : Neg PUnit.{1}

Equations

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

@[simp]

theorem PUnit.one_eq : 1 = unit

@[simp]

theorem PUnit.zero_eq : 0 = unit

theorem PUnit.mul_eq {x y : PUnit.{1}} : x * y = unit

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

@[simp]

theorem PUnit.div_eq {x y : PUnit.{1}} : x / y = unit

@[simp]

theorem PUnit.sub_eq {x y : PUnit.{1}} : x - y = unit

@[simp]

theorem PUnit.inv_eq {x : PUnit.{1}} : x⁻¹ = unit

@[simp]

theorem PUnit.neg_eq {x : PUnit.{1}} : -x = unit

instance PUnit.commRing : CommRing PUnit.{u_1 + 1}

Equations

• PUnit.commRing = CommRing.mk ⋯

instance PUnit.cancelCommMonoidWithZero : CancelCommMonoidWithZero PUnit.{u_1 + 1}

Equations

• PUnit.cancelCommMonoidWithZero = CancelCommMonoidWithZero.mk