Documentation

Mathlib.Algebra.Module.PUnit

Instances on PUnit #

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

source
@[implicit_reducible]
instance PUnit.smul {R : Type u_1} :
SMul R PUnit
source
@[implicit_reducible]
instance PUnit.vadd {R : Type u_1} :
VAdd R PUnit
source
@[simp]
theorem PUnit.smul_eq {R : Type u_3} (y : PUnit) (r : R) :
r • y = unit
source
@[simp]
theorem PUnit.vadd_eq {R : Type u_3} (y : PUnit) (r : R) :
r +ᵥ y = unit
source
instance PUnit.instIsCentralScalar {R : Type u_1} :
IsCentralScalar R PUnit
source
instance PUnit.instIsCentralVAdd {R : Type u_1} :
IsCentralVAdd R PUnit
source
instance PUnit.instSMulCommClass {R : Type u_1} {S : Type u_2} :
SMulCommClass R S PUnit
source
instance PUnit.instVAddCommClass {R : Type u_1} {S : Type u_2} :
VAddCommClass R S PUnit
source
instance PUnit.instIsScalarTowerOfSMul {R : Type u_1} {S : Type u_2} [SMul R S] :
IsScalarTower R S PUnit
source
instance PUnit.instVAddAssocClassOfVAdd {R : Type u_1} {S : Type u_2} [VAdd R S] :
VAddAssocClass R S PUnit
source
@[implicit_reducible]
instance PUnit.smulWithZero {R : Type u_1} [Zero R] :
SMulWithZero R PUnit
source
@[implicit_reducible]
instance PUnit.mulAction {R : Type u_1} [Monoid R] :
MulAction R PUnit
source
@[implicit_reducible]
instance PUnit.distribMulAction {R : Type u_1} [Monoid R] :
DistribMulAction R PUnit
source
@[implicit_reducible]
instance PUnit.mulDistribMulAction {R : Type u_1} [Monoid R] :
MulDistribMulAction R PUnit
source
@[implicit_reducible]
instance PUnit.mulSemiringAction {R : Type u_1} [Semiring R] :
MulSemiringAction R PUnit
source
@[implicit_reducible]
instance PUnit.mulActionWithZero {R : Type u_1} [MonoidWithZero R] :
MulActionWithZero R PUnit
source
@[implicit_reducible]
instance PUnit.module {R : Type u_1} [Semiring R] :
Module R PUnit
source
@[implicit_reducible]
instance PUnit.instSMul_mathlib {R : Type u_1} :
SMul PUnit R
source
@[implicit_reducible]
instance PUnit.instVAdd_mathlib {R : Type u_1} :
VAdd PUnit R
source
@[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.

source
@[simp]
theorem PUnit.vadd_eq' {R : Type u_1} (r : PUnit) (a : R) :
r +ᵥ a = a
source
instance PUnit.instSMulCommClass_1 {R : Type u_1} {S : Type u_2} [SMul R S] :
SMulCommClass PUnit R S
source
instance PUnit.instVAddCommClass_1 {R : Type u_1} {S : Type u_2} [VAdd R S] :
VAddCommClass PUnit R S
source
instance PUnit.instIsScalarTower {R : Type u_1} {S : Type u_2} [SMul R S] :
IsScalarTower PUnit R S
source
@[implicit_reducible]
instance PUnit.instMulAction {R : Type u_1} :
MulAction PUnit R
source
@[implicit_reducible]
instance PUnit.instSMulZeroClass {R : Type u_1} [Zero R] :
SMulZeroClass PUnit R
source
@[implicit_reducible]
instance PUnit.instDistribMulAction {R : Type u_1} [AddMonoid R] :
DistribMulAction PUnit R