Documentation

Mathlib.Algebra.Module.PUnit

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

instance PUnit.vadd {R : Type u_1} :

VAdd R PUnit.{u_3 + 1}

Equations

@[simp]

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

@[simp]

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

r +ᵥ y = unit

instance PUnit.instIsCentralScalar {R : Type u_1} :

IsCentralScalar R PUnit.{u_3 + 1}

instance PUnit.instIsCentralVAdd {R : Type u_1} :

IsCentralVAdd R PUnit.{u_3 + 1}

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

SMulCommClass R S PUnit.{u_3 + 1}

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

VAddCommClass R S PUnit.{u_3 + 1}

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

IsScalarTower R S PUnit.{u_3 + 1}

instance PUnit.instVAddAssocClassOfVAdd {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.{u_3 + 1}

Equations

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

MulAction R PUnit.{u_3 + 1}

Equations

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

DistribMulAction R PUnit.{u_3 + 1}

Equations

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

MulDistribMulAction R PUnit.{u_3 + 1}

Equations

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

MulSemiringAction R PUnit.{u_3 + 1}

Equations

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

MulActionWithZero R PUnit.{u_3 + 1}

Equations

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

Module R PUnit.{u_3 + 1}

Equations

instance PUnit.instSMul_mathlib {R : Type u_1} :

SMul PUnit.{u_3 + 1} R

Equations

instance PUnit.instVAdd_mathlib {R : Type u_1} :

VAdd PUnit.{u_3 + 1} R

Equations

@[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

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

VAddCommClass PUnit.{u_3 + 1} R S

instance 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

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

SMulZeroClass PUnit.{u_3 + 1} R

Equations

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

DistribMulAction PUnit.{u_3 + 1} R

Equations