Documentation

Mathlib.Algebra.Module.PUnit

Instances on PUnit #

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

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

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