# Further results on (semi)linear maps #

instance LinearMap.instSMulDomMulAct {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {S' : Type u_17} [Monoid S'] [] [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' := } }
theorem DomMulAct.smul_linearMap_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {S' : Type u_17} [Monoid S'] [] [SMulCommClass R S' M] (a : S'ᵈᵐᵃ) (f : M →ₛₗ[σ₁₂] M₂) (x : M) :
(a f) x = f (DomMulAct.mk.symm a x)
@[simp]
theorem DomMulAct.mk_smul_linearMap_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {S' : Type u_17} [Monoid S'] [] [SMulCommClass R S' M] (a : S') (f : M →ₛₗ[σ₁₂] M₂) (x : M) :
(DomMulAct.mk a f) x = f (a x)
theorem DomMulAct.coe_smul_linearMap {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {S' : Type u_17} [Monoid S'] [] [SMulCommClass R S' M] (a : S'ᵈᵐᵃ) (f : M →ₛₗ[σ₁₂] M₂) :
(a f) = a f
instance LinearMap.instSMulCommClassDomMulAct {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {S' : Type u_17} {T' : Type u_18} [Monoid S'] [] [SMulCommClass R S' M] [Monoid T'] [] [SMulCommClass R T' M] [SMulCommClass S' T' M] :
Equations
• =
instance LinearMap.instDistribMulActionDomMulActOfSMulCommClass {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {S' : Type u_17} [Monoid S'] [] [SMulCommClass R S' M] :
Equations
• LinearMap.instDistribMulActionDomMulActOfSMulCommClass =
instance LinearMap.instNoZeroSMulDivisors {R : Type u_1} {R₂ : Type u_3} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] [Module S M₂] [SMulCommClass R₂ S M₂] [] :
NoZeroSMulDivisors S (M →ₛₗ[σ₁₂] M₂)
Equations
• =
instance LinearMap.instModuleDomMulActOfSMulCommClass {R : Type u_1} {R₂ : Type u_3} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] [Module S M] [] :
Module Sᵈᵐᵃ (M →ₛₗ[σ₁₂] M₂)
Equations
• LinearMap.instModuleDomMulActOfSMulCommClass =