Further results on (semi)linear maps

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' := ⋯ } }

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 (DomMulAct.mk.symm a • x)

@[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) : (DomMulAct.mk a • f) x = f (a • x)

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

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

Equations

• ⋯ = ⋯

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 = DistribMulAction.mk ⋯ ⋯

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

Equations

• ⋯ = ⋯

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 = Module.mk ⋯ ⋯