# Further results on (semi)linear maps #

source
instance LinearMap.instSMulDomMulAct {R : Type u_1} {R' : Type u_2} {M : Type u_4} {M' : Type u_5} [Semiring R] [Semiring R'] [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R' M'] {σ₁₂ : R →+* R'} {S' : Type u_6} [Monoid S'] [DistribMulAction S' M] [SMulCommClass R S' M] :
SMul S'ᵈᵐᵃ (M →ₛₗ[σ₁₂] M')
Equations

- LinearMap.instSMulDomMulAct = { smul := fun (a : S'ᵈᵐᵃ) (f : M →ₛₗ[σ₁₂] M') => { toFun := a • ⇑f, map_add' := ⋯, map_smul' := ⋯ } }

source
theorem DomMulAct.smul_linearMap_apply {R : Type u_1} {R' : Type u_2} {M : Type u_4} {M' : Type u_5} [Semiring R] [Semiring R'] [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R' M'] {σ₁₂ : R →+* R'} {S' : Type u_6} [Monoid S'] [DistribMulAction S' M] [SMulCommClass R S' M] (a : S'ᵈᵐᵃ) (f : M →ₛₗ[σ₁₂] M') (x : M) :
(a • f) x = f (mk.symm a • x)
source
@[simp]
theorem DomMulAct.mk_smul_linearMap_apply {R : Type u_1} {R' : Type u_2} {M : Type u_4} {M' : Type u_5} [Semiring R] [Semiring R'] [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R' M'] {σ₁₂ : R →+* R'} {S' : Type u_6} [Monoid S'] [DistribMulAction S' M] [SMulCommClass R S' M] (a : S') (f : M →ₛₗ[σ₁₂] M') (x : M) :
(mk a • f) x = f (a • x)
source
theorem DomMulAct.coe_smul_linearMap {R : Type u_1} {R' : Type u_2} {M : Type u_4} {M' : Type u_5} [Semiring R] [Semiring R'] [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R' M'] {σ₁₂ : R →+* R'} {S' : Type u_6} [Monoid S'] [DistribMulAction S' M] [SMulCommClass R S' M] (a : S'ᵈᵐᵃ) (f : M →ₛₗ[σ₁₂] M') :
⇑(a • f) = a • ⇑f
source
instance LinearMap.instSMulCommClassDomMulAct {R : Type u_1} {R' : Type u_2} {M : Type u_4} {M' : Type u_5} [Semiring R] [Semiring R'] [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R' M'] {σ₁₂ : R →+* R'} {S' : Type u_6} {T' : Type u_7} [Monoid S'] [DistribMulAction S' M] [SMulCommClass R S' M] [Monoid T'] [DistribMulAction T' M] [SMulCommClass R T' M] [SMulCommClass S' T' M] :
SMulCommClass S'ᵈᵐᵃ T'ᵈᵐᵃ (M →ₛₗ[σ₁₂] M')
source
instance LinearMap.instDistribMulActionDomMulActOfSMulCommClass {R : Type u_1} {R' : Type u_2} {M : Type u_4} {M' : Type u_5} [Semiring R] [Semiring R'] [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R' M'] {σ₁₂ : R →+* R'} {S' : Type u_6} [Monoid S'] [DistribMulAction S' M] [SMulCommClass R S' M] :
DistribMulAction S'ᵈᵐᵃ (M →ₛₗ[σ₁₂] M')
Equations

- LinearMap.instDistribMulActionDomMulActOfSMulCommClass = { toSMul := LinearMap.instSMulDomMulAct, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }

source
instance LinearMap.instNoZeroSMulDivisors {R : Type u_1} {R' : Type u_2} {S : Type u_3} {M : Type u_4} {M' : Type u_5} [Semiring R] [Semiring R'] [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R' M'] {σ₁₂ : R →+* R'} [Semiring S] [Module S M'] [SMulCommClass R' S M'] [NoZeroSMulDivisors S M'] :
NoZeroSMulDivisors S (M →ₛₗ[σ₁₂] M')
source
instance LinearMap.instModuleDomMulActOfSMulCommClass {R : Type u_1} {R' : Type u_2} {S : Type u_3} {M : Type u_4} {M' : Type u_5} [Semiring R] [Semiring R'] [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R' M'] {σ₁₂ : R →+* R'} [Semiring S] [Module S M] [SMulCommClass R S M] :
Module S ᵈᵐᵃ (M →ₛₗ[σ₁₂] M')
Equations

- LinearMap.instModuleDomMulActOfSMulCommClass = { toDistribMulAction := LinearMap.instDistribMulActionDomMulActOfSMulCommClass, add_smul := ⋯, zero_smul := ⋯ }