Instances on PUnit

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

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 }

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 }

@[simp]

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

@[simp]

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

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

Equations

• ⋯ = ⋯

instance PUnit.instIsCentralVAdd {R : Type u_1} : IsCentralVAdd R 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.instVAddCommClass {R : Type u_1} {S : Type u_2} : VAddCommClass 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.instIsScalarTowerOfVAdd {R : Type u_1} {S : Type u_2} [VAdd R S] : VAddAssocClass R S PUnit.{u_3 + 1}

Equations

• ⋯ = ⋯

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

Equations

• PUnit.smulWithZero = SMulWithZero.mk ⋯

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

Equations

• PUnit.mulAction = MulAction.mk ⋯ ⋯

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

Equations

• PUnit.distribMulAction = DistribMulAction.mk ⋯ ⋯

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

Equations

• PUnit.mulDistribMulAction = MulDistribMulAction.mk ⋯ ⋯

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

Equations

• PUnit.mulSemiringAction = MulSemiringAction.mk ⋯ ⋯

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

Equations

• PUnit.mulActionWithZero = MulActionWithZero.mk ⋯ ⋯

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

Equations

• PUnit.module = Module.mk ⋯ ⋯

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

Equations

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

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

Equations

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

@[simp]

theorem PUnit.smul_eq' {R : Type u_1} (r : PUnit.{u_3 + 1} ) (a : R) : r • a = a

The one-element type acts trivially on every element.

@[simp]

theorem PUnit.vadd_eq' {R : Type u_1} (r : PUnit.{u_3 + 1} ) (a : R) : r +ᵥ a = a

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

instance PUnit.instMulAction {R : Type u_1} : MulAction PUnit.{u_3 + 1} R

Equations

• PUnit.instMulAction = MulAction.mk ⋯ ⋯

instance PUnit.instSMulZeroClass {R : Type u_1} [Zero R] : SMulZeroClass PUnit.{u_3 + 1} R

Equations

• PUnit.instSMulZeroClass = SMulZeroClass.mk ⋯

instance PUnit.instDistribMulAction {R : Type u_1} [AddMonoid R] : DistribMulAction PUnit.{u_3 + 1} R

Equations

• PUnit.instDistribMulAction = DistribMulAction.mk ⋯ ⋯