Documentation

Mathlib.Algebra.PUnitInstances.Module

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

theorem PUnit.instIsCentralScalar {R : Type u_1} :

IsCentralScalar R PUnit.{u_3 + 1}

theorem PUnit.instIsCentralVAdd {R : Type u_1} :

IsCentralVAdd R PUnit.{u_3 + 1}

theorem PUnit.instSMulCommClass {R : Type u_1} {S : Type u_2} :

SMulCommClass R S PUnit.{u_3 + 1}

theorem PUnit.instVAddCommClass {R : Type u_1} {S : Type u_2} :

VAddCommClass R S PUnit.{u_3 + 1}

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

IsScalarTower R S PUnit.{u_3 + 1}

theorem PUnit.instIsScalarTowerOfVAdd {R : Type u_1} {S : Type u_2} [VAdd R S] :

VAddAssocClass R S PUnit.{u_3 + 1}

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

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

SMulCommClass PUnit.{u_3 + 1} R S

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

VAddCommClass PUnit.{u_3 + 1} R S

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

IsScalarTower PUnit.{u_3 + 1} R S

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 ⋯ ⋯