Instances on PUnit

This file collects facts about module structures on the one-element type

instance PUnit.vadd {R : Type u_1} : VAdd R PUnit.{u_3 + 1}

Equations

• PUnit.vadd = { vadd := fun (x : R) (x : PUnit.{?u.2 + 1} ) => PUnit.unit }

instance PUnit.smul {R : Type u_1} : SMul R PUnit.{u_3 + 1}

Equations

• PUnit.smul = { smul := fun (x : R) (x : PUnit.{?u.2 + 1} ) => PUnit.unit }

@[simp]

theorem PUnit.vadd_eq {R : Type u_3} (y : PUnit.{u_4 + 1} ) (r : R) : r +ᵥ y = PUnit.unit

@[simp]

theorem PUnit.smul_eq {R : Type u_3} (y : PUnit.{u_4 + 1} ) (r : R) : r • y = PUnit.unit

instance PUnit.instIsCentralVAdd {R : Type u_1} : IsCentralVAdd R PUnit.{u_3 + 1}

Equations

• ⋯ = ⋯

instance PUnit.instIsCentralScalar {R : Type u_1} : IsCentralScalar R PUnit.{u_3 + 1}

Equations

• ⋯ = ⋯

instance PUnit.instVAddCommClass {R : Type u_1} {S : Type u_2} : VAddCommClass R S PUnit.{u_3 + 1}

Equations

• ⋯ = ⋯

instance PUnit.instSMulCommClass {R : Type u_1} {S : Type u_2} : SMulCommClass R S PUnit.{u_3 + 1}

Equations

• ⋯ = ⋯

instance PUnit.instIsScalarTowerOfVAdd {R : Type u_1} {S : Type u_2} [VAdd R S] : VAddAssocClass R S PUnit.{u_3 + 1}

Equations

• ⋯ = ⋯

instance PUnit.instIsScalarTowerOfSMul {R : Type u_1} {S : Type u_2} [SMul R S] : IsScalarTower R S PUnit.{u_3 + 1}

Equations

• ⋯ = ⋯

instance PUnit.smulWithZero {R : Type u_1} [Zero R] : SMulWithZero R PUnit.{1}

Equations

• PUnit.smulWithZero = let __spread.0 := PUnit.smul; SMulWithZero.mk ⋯

instance PUnit.mulAction {R : Type u_1} [Monoid R] : MulAction R PUnit.{u_3 + 1}

Equations

• PUnit.mulAction = let __spread.0 := PUnit.smul; MulAction.mk ⋯ ⋯

instance PUnit.distribMulAction {R : Type u_1} [Monoid R] : DistribMulAction R PUnit.{u_3 + 1}

Equations

• PUnit.distribMulAction = let __spread.0 := PUnit.mulAction; DistribMulAction.mk ⋯ ⋯

instance PUnit.mulDistribMulAction {R : Type u_1} [Monoid R] : MulDistribMulAction R PUnit.{u_3 + 1}

Equations

• PUnit.mulDistribMulAction = let __spread.0 := PUnit.mulAction; MulDistribMulAction.mk ⋯ ⋯

instance PUnit.mulSemiringAction {R : Type u_1} [Semiring R] : MulSemiringAction R PUnit.{u_3 + 1}

Equations

• PUnit.mulSemiringAction = let __src := PUnit.distribMulAction; let __src_1 := PUnit.mulDistribMulAction; MulSemiringAction.mk ⋯ ⋯

instance PUnit.mulActionWithZero {R : Type u_1} [MonoidWithZero R] : MulActionWithZero R PUnit.{1}

Equations

• PUnit.mulActionWithZero = let __src := PUnit.mulAction; let __src_1 := PUnit.smulWithZero; MulActionWithZero.mk ⋯ ⋯

instance PUnit.module {R : Type u_1} [Semiring R] : Module R PUnit.{u_3 + 1}

Equations

• PUnit.module = let __spread.0 := PUnit.distribMulAction; Module.mk ⋯ ⋯