# Documentation

Mathlib.Algebra.PUnitInstances

# 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), (fun x x => PUnit.unit) 0 x = (fun x x => PUnit.unit) 0 x
Equations
∀ (a b c : PUnit), a + b + c = a + b + c
Equations
• (_ : a + b + c = a + b + c) = (_ : a + b + c = a + b + c)
∀ (a : PUnit), 0 + a = 0 + a
Equations
• (_ : 0 + a = 0 + a) = (_ : 0 + a = 0 + a)
∀ (a : PUnit), a + 0 = a + 0
Equations
• (_ : a + 0 = a + 0) = (_ : a + 0 = a + 0)
∀ (a b : PUnit), a - b = a - b
Equations
• (_ : a - b = a - b) = (_ : a - b = a - b)
∀ (n : ) (a : PUnit), (fun x x => PUnit.unit) () a = (fun x x => PUnit.unit) () a
Equations
• One or more equations did not get rendered due to their size.
∀ (a : PUnit), -a + a = -a + a
Equations
∀ (n : ) (a : PUnit), (fun x x => PUnit.unit) () a = (fun x x => PUnit.unit) () a
Equations
∀ (n : ) (x : PUnit), (fun x x => PUnit.unit) (n + 1) x = (fun x x => PUnit.unit) (n + 1) x
Equations
∀ (a : PUnit), (fun x x => PUnit.unit) 0 a = (fun x x => PUnit.unit) 0 a
Equations
∀ (a b : PUnit), a + b = a + b
Equations
• (_ : a + b = a + b) = (_ : a + b = a + b)
instance PUnit.commGroup :
Equations
@[simp]
theorem PUnit.zero_eq :
@[simp]
theorem PUnit.one_eq :
@[simp]
theorem PUnit.add_eq {x : PUnit} {y : PUnit} :
@[simp]
theorem PUnit.mul_eq {x : PUnit} {y : PUnit} :
@[simp]
theorem PUnit.sub_eq {x : PUnit} {y : PUnit} :
@[simp]
theorem PUnit.div_eq {x : PUnit} {y : PUnit} :
@[simp]
theorem PUnit.neg_eq {x : PUnit} :
@[simp]
theorem PUnit.inv_eq {x : PUnit} :
instance PUnit.commRing :
Equations
Equations
theorem PUnit.gcd_eq {x : PUnit} {y : PUnit} :
theorem PUnit.lcm_eq {x : PUnit} {y : PUnit} :
@[simp]
theorem PUnit.norm_unit_eq {x : PUnit} :
= 1
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
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_1} (y : PUnit) (r : R) :
@[simp]
theorem PUnit.smul_eq {R : Type u_1} (y : PUnit) (r : R) :
Equations
• (_ : ) = (_ : )
Equations
• (_ : ) = (_ : )
Equations
instance PUnit.instSMulCommClassPUnitSmulSmul {R : Type u_1} {S : Type u_2} :
Equations
Equations
Equations
• (_ : ) = (_ : )
instance PUnit.instIsScalarTowerPUnitSmulSmul {R : Type u_1} {S : Type u_2} [inst : SMul R S] :
Equations
instance PUnit.smulWithZero {R : Type u_1} [inst : Zero R] :
Equations
instance PUnit.mulAction {R : Type u_1} [inst : ] :
Equations
instance PUnit.distribMulAction {R : Type u_1} [inst : ] :
Equations
instance PUnit.mulDistribMulAction {R : Type u_1} [inst : ] :
Equations
instance PUnit.mulSemiringAction {R : Type u_1} [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
instance PUnit.mulActionWithZero {R : Type u_1} [inst : ] :
Equations
• PUnit.mulActionWithZero = let src := PUnit.mulAction; let src_1 := PUnit.smulWithZero; MulActionWithZero.mk (_ : ∀ (a : R), a 0 = 0) (_ : ∀ (m : PUnit), 0 m = 0)
instance PUnit.module {R : Type u_1} [inst : ] :
Equations