Instances on PUnit

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

@[implicit_reducible]

instance PUnit.smul {R : Type u_1} : SMul R PUnit

Equations

• PUnit.smul = { smul := fun (x : R) (x_1 : PUnit) => PUnit.unit }

@[implicit_reducible]

instance PUnit.vadd {R : Type u_1} : VAdd R PUnit

Equations

• PUnit.vadd = { vadd := fun (x : R) (x_1 : PUnit) => PUnit.unit }

@[simp]

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

@[simp]

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

instance PUnit.instIsCentralScalar {R : Type u_1} : IsCentralScalar R PUnit

instance PUnit.instIsCentralVAdd {R : Type u_1} : IsCentralVAdd R PUnit

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

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

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

instance PUnit.instVAddAssocClassOfVAdd {R : Type u_1} {S : Type u_2} [VAdd R S] : VAddAssocClass R S PUnit

@[implicit_reducible]

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

Equations

• PUnit.smulWithZero = { toSMul := PUnit.smul, smul_zero := ⋯, zero_smul := ⋯ }

@[implicit_reducible]

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

Equations

• PUnit.mulAction = { toSMul := PUnit.smul, mul_smul := ⋯, one_smul := ⋯ }

@[implicit_reducible]

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

Equations

• PUnit.distribMulAction = { toMulAction := PUnit.mulAction, smul_zero := ⋯, smul_add := ⋯ }

@[implicit_reducible]

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

Equations

• PUnit.mulDistribMulAction = { toMulAction := PUnit.mulAction, smul_mul := ⋯, smul_one := ⋯ }

@[implicit_reducible]

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

Equations

• PUnit.mulSemiringAction = { toDistribMulAction := PUnit.distribMulAction, smul_one := ⋯, smul_mul := ⋯ }

@[implicit_reducible]

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

Equations

• PUnit.mulActionWithZero = { toMulAction := PUnit.mulAction, smul_zero := ⋯, zero_smul := ⋯ }

@[implicit_reducible]

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

Equations

• PUnit.module = { toDistribMulAction := PUnit.distribMulAction, add_smul := ⋯, zero_smul := ⋯ }

@[implicit_reducible]

instance PUnit.instSMul_mathlib {R : Type u_1} : SMul PUnit R

Equations

• PUnit.instSMul_mathlib = { smul := fun (x : PUnit) (x_1 : R) => x_1 }

@[implicit_reducible]

instance PUnit.instVAdd_mathlib {R : Type u_1} : VAdd PUnit R

Equations

• PUnit.instVAdd_mathlib = { vadd := fun (x : PUnit) (x_1 : R) => x_1 }

@[simp]

theorem PUnit.smul_eq' {R : Type u_1} (r : PUnit) (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) (a : R) : r +ᵥ a = a

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

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

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

@[implicit_reducible]

instance PUnit.instMulAction {R : Type u_1} : MulAction PUnit R

Equations

• PUnit.instMulAction = { toSMul := inferInstance, mul_smul := ⋯, one_smul := ⋯ }

@[implicit_reducible]

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

Equations

• PUnit.instSMulZeroClass = { toSMul := inferInstance, smul_zero := ⋯ }

@[implicit_reducible]

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

Equations

• PUnit.instDistribMulAction = { toMulAction := inferInstance, smul_zero := ⋯, smul_add := ⋯ }