# Instances on PUnit #

This file collects facts about algebraic structures on the one-element type, e.g. that it is a commutative ring.

∀ (x : PUnit.{u_1 + 1} ), (fun (x : ) (x : PUnit.{u_1 + 1} ) => PUnit.unit) 0 x = (fun (x : ) (x : PUnit.{u_1 + 1} ) => PUnit.unit) 0 x
∀ (a b : PUnit.{u_1 + 1} ), a - b = a - b
∀ (n : ) (a : PUnit.{u_1 + 1} ), (fun (x : ) (x : PUnit.{u_1 + 1} ) => PUnit.unit) () a = (fun (x : ) (x : PUnit.{u_1 + 1} ) => PUnit.unit) () a
∀ (a : PUnit.{u_1 + 1} ), (fun (x : ) (x : PUnit.{u_1 + 1} ) => PUnit.unit) 0 a = (fun (x : ) (x : PUnit.{u_1 + 1} ) => PUnit.unit) 0 a
∀ (n : ) (a : PUnit.{u_1 + 1} ), (fun (x : ) (x : PUnit.{u_1 + 1} ) => PUnit.unit) (Int.ofNat n.succ) a = (fun (x : ) (x : PUnit.{u_1 + 1} ) => PUnit.unit) (Int.ofNat n.succ) a
∀ (a b c : PUnit.{u_1 + 1} ), a + b + c = a + b + c
∀ (n : ) (x : PUnit.{u_1 + 1} ), (fun (x : ) (x : PUnit.{u_1 + 1} ) => PUnit.unit) (n + 1) x = (fun (x : ) (x : PUnit.{u_1 + 1} ) => PUnit.unit) (n + 1) x
∀ (a b : PUnit.{u_1 + 1} ), a + b = a + b
instance PUnit.instZero :
Equations
instance PUnit.instOne :
Equations
Equations
Equations
Equations
Equations
instance PUnit.instNeg :
Equations
instance PUnit.instInv :
Equations
@[simp]
theorem PUnit.zero_eq :
@[simp]
theorem PUnit.one_eq :
@[simp]
theorem PUnit.sub_eq {x : PUnit.{1}} {y : PUnit.{1}} :
@[simp]
theorem PUnit.div_eq {x : PUnit.{1}} {y : PUnit.{1}} :
@[simp]
theorem PUnit.neg_eq {x : PUnit.{1}} :
@[simp]
theorem PUnit.inv_eq {x : PUnit.{1}} :
instance PUnit.commRing :
Equations
Equations
@[simp]
Equations
• One or more equations did not get rendered due to their size.
instance PUnit.vadd {R : Type u_1} :
Equations
instance PUnit.smul {R : Type u_1} :
Equations
@[simp]
theorem PUnit.vadd_eq {R : Type u_3} (y : PUnit.{u_4 + 1} ) (r : R) :
@[simp]
theorem PUnit.smul_eq {R : Type u_3} (y : PUnit.{u_4 + 1} ) (r : R) :
instance PUnit.instIsCentralVAdd {R : Type u_1} :
Equations
• =
instance PUnit.instIsCentralScalar {R : Type u_1} :
Equations
• =
instance PUnit.instVAddCommClass {R : Type u_1} {S : Type u_2} :
Equations
• =
instance PUnit.instSMulCommClass {R : Type u_1} {S : Type u_2} :
Equations
• =
instance PUnit.instIsScalarTowerOfVAdd {R : Type u_1} {S : Type u_2} [VAdd R S] :
Equations
• =
instance PUnit.instIsScalarTowerOfSMul {R : Type u_1} {S : Type u_2} [SMul R S] :
Equations
• =
instance PUnit.smulWithZero {R : Type u_1} [Zero R] :
Equations
• PUnit.smulWithZero = let __spread.0 := PUnit.smul;
instance PUnit.mulAction {R : Type u_1} [] :
Equations
• PUnit.mulAction = let __spread.0 := PUnit.smul;
instance PUnit.distribMulAction {R : Type u_1} [] :
Equations
• PUnit.distribMulAction = let __spread.0 := PUnit.mulAction;
instance PUnit.mulDistribMulAction {R : Type u_1} [] :
Equations
• PUnit.mulDistribMulAction = let __spread.0 := PUnit.mulAction;
instance PUnit.mulSemiringAction {R : Type u_1} [] :
Equations
• PUnit.mulSemiringAction = let __src := PUnit.distribMulAction; let __src_1 := PUnit.mulDistribMulAction;
instance PUnit.mulActionWithZero {R : Type u_1} [] :
Equations
• PUnit.mulActionWithZero = let __src := PUnit.mulAction; let __src_1 := PUnit.smulWithZero;
instance PUnit.module {R : Type u_1} [] :
Equations
• PUnit.module = let __spread.0 := PUnit.distribMulAction;