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.

source
🔸 coverage
@[implicit_reducible]
instance PUnit.commGroup :
CommGroup PUnit.{u_1 + 1}
source
🔸 coverage
@[implicit_reducible]
instance PUnit.addCommGroup :
AddCommGroup PUnit.{u_1 + 1}
source
🔸 coverage
@[implicit_reducible]
instance PUnit.instOne_mathlib :
One PUnit.{u_1 + 1}
source
🔸 coverage
@[implicit_reducible]
instance PUnit.instZero_mathlib :
Zero PUnit.{u_1 + 1}
source
🔸 coverage
@[implicit_reducible]
instance PUnit.instMul_mathlib :
Mul PUnit.{u_1 + 1}
source
🔸 coverage
@[implicit_reducible]
instance PUnit.instAdd_mathlib :
Add PUnit.{u_1 + 1}
source
🔸 coverage
@[implicit_reducible]
instance PUnit.instDiv_mathlib :
Div PUnit.{u_1 + 1}
source
🔸 coverage
@[implicit_reducible]
instance PUnit.instSub_mathlib :
Sub PUnit.{u_1 + 1}
source
🔸 coverage
@[implicit_reducible]
instance PUnit.instInv_mathlib :
Inv PUnit.{u_1 + 1}
source
🔸 coverage
@[implicit_reducible]
instance PUnit.instNeg_mathlib :
Neg PUnit.{u_1 + 1}
source
📐 coverage
@[simp]
theorem PUnit.one_eq :
1 = unit
source
📐 coverage
@[simp]
theorem PUnit.zero_eq :
0 = unit
source
📐 coverage
theorem PUnit.mul_eq (x y : PUnit.{u_1 + 1}) :
x * y = unit
source
📐 coverage
theorem PUnit.add_eq (x y : PUnit.{u_1 + 1}) :
x + y = unit
source
📐 coverage
@[simp]
theorem PUnit.div_eq (x y : PUnit.{u_1 + 1}) :
x / y = unit
source
📐 coverage
@[simp]
theorem PUnit.sub_eq (x y : PUnit.{u_1 + 1}) :
x - y = unit
source
📐 coverage
@[simp]
theorem PUnit.inv_eq (x : PUnit.{u_1 + 1}) :
x⁻¹ = unit
source
📐 coverage
@[simp]
theorem PUnit.neg_eq (x : PUnit.{u_1 + 1}) :
-x = unit