Instances on PUnit #
This file collects facts about algebraic structures on the one-element type, e.g. that it is a commutative ring.
def
PUnit.addCommGroup.proof_4 :
∀ (x : PUnit), (fun x x => PUnit.unit) 0 x = (fun x x => PUnit.unit) 0 x
Equations
- (_ : (fun x x => PUnit.unit) 0 x = (fun x x => PUnit.unit) 0 x) = (_ : (fun x x => PUnit.unit) 0 x = (fun x x => PUnit.unit) 0 x)
def
PUnit.addCommGroup.proof_8 :
∀ (n : ℕ) (a : PUnit),
(fun x x => PUnit.unit) (Int.ofNat (Nat.succ n)) a = (fun x x => PUnit.unit) (Int.ofNat (Nat.succ n)) a
Equations
- One or more equations did not get rendered due to their size.
def
PUnit.addCommGroup.proof_9 :
∀ (n : ℕ) (a : PUnit), (fun x x => PUnit.unit) (Int.negSucc n) a = (fun x x => PUnit.unit) (Int.negSucc n) a
Equations
- (_ : (fun x x => PUnit.unit) (Int.negSucc n) a = (fun x x => PUnit.unit) (Int.negSucc n) a) = (_ : (fun x x => PUnit.unit) (Int.negSucc n) a = (fun x x => PUnit.unit) (Int.negSucc n) a)
def
PUnit.addCommGroup.proof_5 :
∀ (n : ℕ) (x : PUnit), (fun x x => PUnit.unit) (n + 1) x = (fun x x => PUnit.unit) (n + 1) x
Equations
- (_ : (fun x x => PUnit.unit) (n + 1) x = (fun x x => PUnit.unit) (n + 1) x) = (_ : (fun x x => PUnit.unit) (n + 1) x = (fun x x => PUnit.unit) (n + 1) x)
def
PUnit.addCommGroup.proof_7 :
∀ (a : PUnit), (fun x x => PUnit.unit) 0 a = (fun x x => PUnit.unit) 0 a
Equations
- (_ : (fun x x => PUnit.unit) 0 a = (fun x x => PUnit.unit) 0 a) = (_ : (fun x x => PUnit.unit) 0 a = (fun x x => PUnit.unit) 0 a)
Equations
- PUnit.commRing = let src := PUnit.commGroup; let src_1 := PUnit.addCommGroup; CommRing.mk (_ : ∀ (a b : PUnit), a * b = b * a)
Equations
- PUnit.cancelCommMonoidWithZero = let src := PUnit.commRing; CancelCommMonoidWithZero.mk
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.
Equations
- PUnit.vadd = { vadd := fun x x => PUnit.unit }
Equations
- PUnit.smul = { smul := fun x x => PUnit.unit }
Equations
- (_ : IsCentralVAdd R PUnit) = (_ : IsCentralVAdd R PUnit)
def
PUnit.instVAddCommClassPUnitVaddVadd.proof_1
{R : Type u_1}
{S : Type u_2}
:
VAddCommClass R S PUnit
Equations
- (_ : VAddCommClass R S PUnit) = (_ : VAddCommClass R S PUnit)
instance
PUnit.instVAddCommClassPUnitVaddVadd
{R : Type u_1}
{S : Type u_2}
:
VAddCommClass R S PUnit
instance
PUnit.instSMulCommClassPUnitSmulSmul
{R : Type u_1}
{S : Type u_2}
:
SMulCommClass R S PUnit
instance
PUnit.instIsScalarTowerPUnitVaddVadd
{R : Type u_1}
{S : Type u_2}
[inst : VAdd R S]
:
VAddAssocClass R S PUnit
def
PUnit.instIsScalarTowerPUnitVaddVadd.proof_1
{R : Type u_1}
{S : Type u_2}
[inst : VAdd R S]
:
VAddAssocClass R S PUnit
Equations
- (_ : VAddAssocClass R S PUnit) = (_ : VAddAssocClass R S PUnit)
instance
PUnit.instIsScalarTowerPUnitSmulSmul
{R : Type u_1}
{S : Type u_2}
[inst : SMul R S]
:
IsScalarTower R S PUnit
Equations
- PUnit.smulWithZero = let src := PUnit.smul; SMulWithZero.mk (_ : ∀ (m : PUnit), 0 • m = 0)
Equations
- One or more equations did not get rendered due to their size.