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

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) :

@[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.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.{u_3 + 1}

Equations

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

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

MulAction R PUnit.{u_3 + 1}

Equations

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

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

DistribMulAction R PUnit.{u_3 + 1}

Equations

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

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

MulDistribMulAction R PUnit.{u_3 + 1}

Equations

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

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

MulSemiringAction R PUnit.{u_3 + 1}

Equations

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

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

MulActionWithZero R PUnit.{u_3 + 1}

Equations

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

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

Module R PUnit.{u_3 + 1}

Equations

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

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

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

PUnit.instMulAction = { toSMul := inferInstanceAs (SMul PUnit.{?u.7 + 1} R), one_smul := ⋯, mul_smul := ⋯ }

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

SMulZeroClass PUnit.{u_3 + 1} R

Equations

PUnit.instSMulZeroClass = { toSMul := inferInstanceAs (SMul PUnit.{?u.11 + 1} R), smul_zero := ⋯ }

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

DistribMulAction PUnit.{u_3 + 1} R

Equations

PUnit.instDistribMulAction = { toMulAction := inferInstanceAs (MulAction PUnit.{?u.11 + 1} R), smul_zero := ⋯, smul_add := ⋯ }